English
Given a function m: α → β and a realizer F for a filter f on β, there is a realizer for comap m f with base s ↦ preimage m (F.F s).
Русский
Для отображения comap m f существует реализатор с основанием s ↦ preimage m (F.F s).
LaTeX
$$$\\mathrm{Realizer.comap}(m)(F) : (\\mathrm{Filter.comap}\\ m\\ f).Realizer$ with $\\mathrm{f} := s \\mapsto \\mathrm{preimage}(m, F.F(s))$.$$
Lean4
/-- Construct a realizer for `comap m f` given a realizer for `f` -/
protected def comap (m : α → β) {f : Filter β} (F : f.Realizer) : (comap m f).Realizer :=
⟨F.σ,
{ f := fun s ↦ preimage m (F.F s)
pt := F.F.pt
inf := F.F.inf
inf_le_left := fun _ _ ↦ preimage_mono (F.F.inf_le_left _ _)
inf_le_right := fun _ _ ↦ preimage_mono (F.F.inf_le_right _ _) },
filter_eq <|
Set.ext fun _ ↦ by
cases F; subst f
exact ⟨fun ⟨s, h⟩ ↦ ⟨_, ⟨s, Subset.refl _⟩, h⟩, fun ⟨_, ⟨s, h⟩, h₂⟩ ↦ ⟨s, Subset.trans (preimage_mono h) h₂⟩⟩⟩
