disjoint_opensRange_sigmaι — Mathlib

English

If i ≠ j, the open ranges (Sigma.ι f i).opensRange and (Sigma.ι f j).opensRange are disjoint.

Русский

Если i ≠ j, открытые диапазоны (Sigma.ι f i).opensRange и (Sigma.ι f j).opensRange попарно непересекаются.

LaTeX

$$$\\mathrm{Disjoint}\\big((\\Sigma.ι f i).\\text{opensRange}, (\\Sigma.ι f j).\\text{opensRange}\\big)$ for $i \\neq j$$$

Lean4

/-- The images of each component in the coproduct is disjoint. -/
theorem disjoint_opensRange_sigmaι (i j : ι) (h : i ≠ j) : Disjoint (Sigma.ι f i).opensRange (Sigma.ι f j).opensRange :=
  by
  intro U hU hU' x hx
  obtain ⟨x, rfl⟩ := hU hx
  obtain ⟨y, hy⟩ := hU' hx
  obtain ⟨rfl⟩ := (sigmaι_eq_iff _ _ _ _ _).mp hy
  cases h rfl

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