mem_comap — Mathlib

English

For any injective m and large ∈ u, membership in the pulled-back ultrafilter equals membership of the image: s ∈ u.comap inj large iff m '' s ∈ u.

Русский

Членство в вытянутом назад ультрафильтре через инъекцию равно членству в образе: s ∈ u.comap inj large ⇔ m''s ∈ u.

LaTeX

$$$ s \in u.comap inj large \iff m '' s \in u $$$

Lean4

@[simp]
theorem mem_comap {m : α → β} (u : Ultrafilter β) (inj : Injective m) (large : Set.range m ∈ u) {s : Set α} :
    s ∈ u.comap inj large ↔ m '' s ∈ u :=
  mem_comap_iff inj large

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