filter_map_top — Mathlib

English

For a subset s of α, map (Subtype.val) (comap Subtype.val f) = f ⊓ 𝓟 s.

Русский

Для подмножества s ⊆ α отображение через включение в α даёт: map Subtype.val (comap Subtype.val f) = f ⊓ 𝓟 s.

LaTeX

$$$ \\operatorname{map}(\\operatorname{Subtype.val}) (\\operatorname{comap}(\\operatorname{Subtype.val}) f) = f \\; \\inf \\; 𝓟 s $$$

Lean4

theorem _root_.Function.Surjective.filter_map_top {f : α → β} (hf : Surjective f) : map f ⊤ = ⊤ :=
  (congr_arg _ comap_top).symm.trans <| map_comap_of_surjective hf ⊤

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