mem_comap_iff — Mathlib

English

For injective m and large range m ∈ f, S ∈ comap m f iff m''S ∈ f.

Русский

Для инъективного m и большого range m ∈ f: S ∈ comap m f тогда и только тогда, как m''S ∈ f.

LaTeX

$$$ S \\in comap m f \\; \\iff \\; m '' S \\in f $$$

Lean4

theorem mem_comap_iff {f : Filter β} {m : α → β} (inj : Injective m) (large : Set.range m ∈ f) {S : Set α} :
    S ∈ comap m f ↔ m '' S ∈ f := by rw [← image_mem_map_iff inj, map_comap_of_mem large]

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