English
Transfer a filter realizer along an equivalence on the base type: (F.ofEquiv E) reindexes the base σ to τ and reuses F.F with renaming.
Русский
Перенос реализатора фильтра вдоль эквиваленции базы: (F.ofEquiv E) переиндексирует базу σ на τ и использует F.F с переименованием.
LaTeX
$$$F\\mapsto F.ofEquiv(E)$ defines a realizer for the same filter with index renamed by $E$.$$
Lean4
/-- Transfer a filter realizer to another realizer on a different base type. -/
def ofEquiv {f : Filter α} (F : f.Realizer) (E : F.σ ≃ τ) : f.Realizer :=
⟨τ, F.F.ofEquiv E, by
refine Eq.trans ?_ F.eq
exact filter_eq (Set.ext fun _ ↦ ⟨fun ⟨s, h⟩ ↦ ⟨E.symm s, by simpa using h⟩, fun ⟨t, h⟩ ↦ ⟨E t, by simp [h]⟩⟩)⟩
