disjoint_comap_iff — Mathlib

English

For a surjective map m, disjointness of comaps is equivalent to disjointness of the original filters.

Русский

Для сюръективного отображения m дизjointность отображений через m эквивалентна дизjointности исходных фильтров.

LaTeX

$$$\\mathrm{Disjoint}(\\operatorname{comap} m\, g_1, \\operatorname{comap} m\, g_2) \\iff \\mathrm{Disjoint}(g_1,g_2)$$$

Lean4

theorem disjoint_comap_iff (h : Surjective m) : Disjoint (comap m g₁) (comap m g₂) ↔ Disjoint g₁ g₂ := by
  rw [disjoint_iff, disjoint_iff, ← comap_inf, comap_surjective_eq_bot h]

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