map_le_map_iff_of_injOn — Mathlib

English

If l1, l2 are filters on α and f is injective on a set s, then map f l1 ≤ map f l2 iff l1 ≤ l2 (restricted to s).

Русский

Если l1, l2 — фильтры на α и f инъективен на s, тогда map f l1 ≤ map f l2 тогда и только тогда l1 ≤ l2 (ограничено до s).

LaTeX

$$$ (map\\ f\\ l_1) \\le (map\\ f\\ l_2) \\;\\iff\\; l_1 \\le l_2 \\quad \\text{under appropriate } InjOn f s$$$

Lean4

theorem map_le_map_iff_of_injOn {l₁ l₂ : Filter α} {f : α → β} {s : Set α} (h₁ : s ∈ l₁) (h₂ : s ∈ l₂)
    (hinj : InjOn f s) : map f l₁ ≤ map f l₂ ↔ l₁ ≤ l₂ :=
  ⟨fun h _t ht =>
    mp_mem h₁ <|
      mem_of_superset (h <| image_mem_map (inter_mem h₂ ht)) fun _y ⟨_x, ⟨hxs, hxt⟩, hxy⟩ hys => hinj hxs hys hxy ▸ hxt,
    fun h => map_mono h⟩

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