English
A filter realizes itself via its own base: the Realizer.ofFilter f uses f.sets as the base, the function f := Subtype.val, and point univ, with intersections given by inter.
Русский
Фильтр реализуется самим своим основанием: Realizer.ofFilter f использует f.sets как основание, функцию f := Subtype.val и точку univ, пересечения задаются через inter.
LaTeX
$$$\\mathrm{ofFilter}(f) = \\langle f.{\\tt sets}, \\{ f := \\mathrm{Subtype}.val, \\; pt := (\\mathrm{univ},\\mathrm{univ\_mem}), \\; inf := (\\langle \\_,\\_ \\rangle),\\;\\dots \\}, \\text{filter\_eq}(\\dots)\\rangle$$$
Lean4
/-- Transfer a realizer along an equality of filter. This has better definitional equalities than
the `Eq.rec` proof. -/
def ofEq {f g : Filter α} (e : f = g) (F : f.Realizer) : g.Realizer :=
⟨F.σ, F.F, F.eq.trans e⟩
