filter_injOn_Iic_iff_injOn — Mathlib

English

InjOn (map m) (Iic 𝓟 s) is equivalent to InjOn m s.

Русский

Инъективность отображения на Iic 𝓟 s эквивалентна инъективности отображения m на s.

LaTeX

$$$\\mathrm{InjOn}(\\mathrm{map}\\, m)\\,(\\mathrm{Iic}\\,\\mathcal{P} s) \\iff \\mathrm{InjOn}\, m\, s$$$

Lean4

theorem filter_injOn_Iic_iff_injOn {s : Set α} {m : α → β} : InjOn (map m) (Iic <| 𝓟 s) ↔ InjOn m s :=
  by
  refine ⟨fun hm x hx y hy hxy ↦ ?_, fun hm F hF G hG ↦ ?_⟩
  ·
    rwa [← pure_injective.eq_iff, ← map_pure, ← map_pure, hm.eq_iff, pure_injective.eq_iff] at hxy <;>
      rwa [mem_Iic, pure_le_principal]
  · simp [map_eq_map_iff_of_injOn (le_principal_iff.mp hF) (le_principal_iff.mp hG) hm]

Похожие утверждения