English
Given a function m: α → β and a realizer F for f, there is a realizer for the mapped filter map m f, whose base is s ↦ image m (F.F s).
Русский
Задаётся реализатор для отображённого фильтра map m f, где основание задаётся как s ↦ image m (F.F s).
LaTeX
$$$\\mathrm{Realizer.map}(m)(F) : (\\mathrm{Filter.map}\\ m\\ f).Realizer$ with $\\mathrm{F}.f(s)\\mapsto \\mathrm{image}\\ m (F.F(s))$.$$
Lean4
/-- Construct a realizer for `map m f` given a realizer for `f` -/
protected def map (m : α → β) {f : Filter α} (F : f.Realizer) : (map m f).Realizer :=
⟨F.σ,
{ f := fun s ↦ image m (F.F s)
pt := F.F.pt
inf := F.F.inf
inf_le_left := fun _ _ ↦ image_mono (F.F.inf_le_left _ _)
inf_le_right := fun _ _ ↦ image_mono (F.F.inf_le_right _ _) },
filter_eq <|
Set.ext fun _ ↦
by
simp only [CFilter.toFilter, image_subset_iff, mem_setOf_eq, Filter.mem_sets, mem_map]
rw [F.mem_sets]⟩
