mem_map — Mathlib

English

For any function m, ultrafilter f on α, and subset s of β, we have s ∈ map m f if and only if m^{-1}(s) ∈ f.

Русский

Для любой функции m, ультрафильтра f на α и подмножества s ⊆ β верно: s ∈ map m f тогда и только тогда, когда m^{-1}(s) ∈ f.

LaTeX

$$$ s \in map m f \iff m^{-1} s \in f $$$

Lean4

@[simp]
theorem mem_map {m : α → β} {f : Ultrafilter α} {s : Set β} : s ∈ map m f ↔ m ⁻¹' s ∈ f :=
  Iff.rfl

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