English
Characterizes surjectivity of map with respect to downward-closed principal filters: SurjOn (map m) (Iic F) (Iic G) iff G ≤ map m F.
Русский
Характеризует сюръективность отображения относительно нисходящих примитивных фильтров: SurjOn (map m) (Iic F) (Iic G) эквивалентно G ≤ map m F.
LaTeX
$$$\\mathrm{SurjOn}(\\mathrm{map}\\, m)\\,(Iic\\,F)\\,(Iic\\,G) \\iff G \\leq \\mathrm{map}\\, m\\, F$$$
Lean4
theorem map_surjOn_Iic_iff_le_map {m : α → β} : SurjOn (map m) (Iic F) (Iic G) ↔ G ≤ map m F :=
by
refine ⟨fun hm ↦ ?_, fun hm ↦ ?_⟩
· rcases hm right_mem_Iic with ⟨H, (hHF : H ≤ F), rfl⟩
exact map_mono hHF
· have : RightInvOn (F ⊓ comap m ·) (map m) (Iic G) := fun H (hHG : H ≤ G) ↦ by
simpa [Filter.push_pull] using hHG.trans hm
exact this.surjOn fun H _ ↦ mem_Iic.mpr inf_le_left
