mem_toFilter_sets — Mathlib

English

Membership in the toFilter of a CFilter is equivalent to the base-existential condition: a ∈ F.toFilter ⇔ ∃ b, F.b ⊆ a.

Русский

Членство в F.toFilter эквивалентно существованию базового элемента: a ∈ F.toFilter ⇔ ∃ b, F b ⊆ a.

LaTeX

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

Lean4

@[simp]
theorem mem_toFilter_sets (F : CFilter (Set α) σ) {a : Set α} : a ∈ F.toFilter ↔ ∃ b, F b ⊆ a :=
  Iff.rfl

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