isCompl_opensRange_inl_inr — Mathlib

English

The two opens corresponding to the left and right injections form a complemented pair.

Русский

Две открытые подмножества, соответствующие Inl и Inr, образуют дополняемую пару.

LaTeX

$$$IsCompl\\big(coprod.inl.opensRange, coprod.inr.opensRange\\big)$$$

Lean4

theorem isCompl_opensRange_inl_inr : IsCompl (coprod.inl : X ⟶ X ⨿ Y).opensRange (coprod.inr : Y ⟶ X ⨿ Y).opensRange :=
  by
  convert isCompl_range_inl_inr X Y
  simp only [isCompl_iff, disjoint_iff, codisjoint_iff, ← TopologicalSpace.Opens.coe_inj]
  rfl

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