disjoint_comap — Mathlib

English

Disjointness is preserved by pullback: if g1 and g2 are disjoint on β, then comap m g1 and comap m g2 are disjoint on α.

Русский

Несопоставимость сохраняется при обратном изображении: если g1 и g2 непересекаются на β, то comap m g1 и comap m g2 непересекаются на α.

LaTeX

$$$ \\operatorname{Disjoint}(g_1,g_2) \\Rightarrow \\operatorname{Disjoint}(\\operatorname{comap}_m g_1, \\operatorname{comap}_m g_2) $$$

Lean4

theorem disjoint_comap (h : Disjoint g₁ g₂) : Disjoint (comap m g₁) (comap m g₂) := by
  simp only [disjoint_iff, ← comap_inf, h.eq_bot, comap_bot]

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