comap_pure — Mathlib

English

Pullback of a principal ultrafilter along the injection from a to m a with large range is the principal ultrafilter at a.

Русский

Вытянутая назад главного ультрафильтра через отображение, переводящее a к m a, даёт главный ультрафильтр на a.

LaTeX

$$$ comap (pure <| m a) inj large = pure a $$$

Lean4

@[simp]
theorem comap_pure {m : α → β} (a : α) (inj : Injective m) (large) : comap (pure <| m a) inj large = pure a :=
  coe_injective <|
    Filter.comap_pure.trans <| by rw [coe_pure, ← principal_singleton, ← image_singleton, preimage_image_eq _ inj]

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