eq_of_not_disjoint_openCell — Mathlib

English

If two open cells from possibly different indices are not disjoint, then they are the same cell: ⟨n,j⟩ = ⟨m,i⟩.

Русский

Если две открытые клетки не дизъюнктны, значит это одна и та же клетка: ⟨n,j⟩ = ⟨m,i⟩.

LaTeX

$$$\neg Disjoint (openCell n j) (openCell m i) \Rightarrow (\langle n, j\rangle = \langle m, i\rangle)$$$

Lean4

/-- The contrapositive of `disjoint_openCell_of_ne`. -/
theorem eq_of_not_disjoint_openCell [RelCWComplex C D] {n : ℕ} {j : cell C n} {m : ℕ} {i : cell C m}
    (h : ¬Disjoint (openCell n j) (openCell m i)) : (⟨n, j⟩ : (Σ n, cell C n)) = ⟨m, i⟩ :=
  by
  contrapose! h
  exact disjoint_openCell_of_ne h

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