coe_comap — Mathlib

English

The underlying Filter of the pullback ultrafilter equals the pullback Filter along m: (u.comap inj large : Filter α) = Filter.comap m u.

Русский

Основа фильтра вытянутого назад ультрафильтра совпадает с фильтром, полученным вытягиванием по m: (u.comap inj large : Filter α) = Filter.comap m u.

LaTeX

$$$ (u.comap inj large : Filter \alpha) = Filter.comap m u $$$

Lean4

@[simp, norm_cast]
theorem coe_comap {m : α → β} (u : Ultrafilter β) (inj : Injective m) (large : Set.range m ∈ u) :
    (u.comap inj large : Filter α) = Filter.comap m u :=
  rfl

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