toRealizer — Mathlib

English

Equality between the explicit toFilter construction and the canonical toFilter data yields that F.toFilter is exactly the filter generated by its base data.

Русский

Свойство равенства между явной конструкцией toFilter и каноническими данными toFilter говорит, что F.toFilter порождается именно базой.

LaTeX

$$$F^{toFilter}=\\text{Filter}\\left(\\{a\\subseteq α: ∃ b, F b \\subseteq a\\}\\right)\\,.$$$

Lean4

/-- A `CFilter` realizes the filter it generates. -/
protected def toRealizer (F : CFilter (Set α) σ) : F.toFilter.Realizer :=
  ⟨σ, F, rfl⟩

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