mem_sets — Mathlib

English

For a Realizer F of a filter f, membership a ∈ f is equivalent to the existence of a base element b with F.F b ⊆ a.

Русский

Для реализатора F фильтра f членство a ∈ f эквивалентно существованию базового элемента b с F.F b ⊆ a.

LaTeX

$$$a\\in f \\iff \\exists b, F.F b \\subseteq a$.$$

Lean4

theorem mem_sets {f : Filter α} (F : f.Realizer) {a : Set α} : a ∈ f ↔ ∃ b, F.F b ⊆ a := by cases F; subst f; rfl

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