exists_mem_subset_iff — Mathlib

English

The membership of a set s in a filter f is equivalent to the existence of a member t of f with t ⊆ s.

Русский

Принадлежность множества s фильтру f эквивалентна существованию элемента t в f, такого что t ⊆ s.

LaTeX

$$$ (\exists t \in f,\ t \subseteq s) \iff s \in f. $$$

Lean4

theorem exists_mem_subset_iff : (∃ t ∈ f, t ⊆ s) ↔ s ∈ f :=
  ⟨fun ⟨_, ht, ts⟩ => mem_of_superset ht ts, fun hs => ⟨s, hs, Subset.rfl⟩⟩

Похожие утверждения