comap_le_comap_iff — Mathlib

English

For a set s of filters on β, comap m of the supremum equals the supremum of comaps: comap m (sSup s) = ⨆ f ∈ s, comap m f.

Русский

Для множества фильтров s на β справедливо: comap m (sSup s) = ⨆ f ∈ s, comap m f.

LaTeX

$$$ \\operatorname{comap}_m( \\mathrm{sSup}(s) ) = \\bigvee_{f \\in s} \\operatorname{comap}_m f $$$

Lean4

theorem comap_le_comap_iff {f g : Filter β} {m : α → β} (hf : range m ∈ f) : comap m f ≤ comap m g ↔ f ≤ g :=
  ⟨fun h => map_comap_of_mem hf ▸ (map_mono h).trans map_comap_le, fun h => comap_mono h⟩

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