coe_ne_coe — Mathlib

English

For all x,y ∈ α, (x : ConnectedComponents α) ≠ y iff connectedComponent(x) ≠ connectedComponent(y).

Русский

Для всех x,y ∈ α: (x : ConnectedComponents α) ≠ y эквивалентно connectedComponent(x) ≠ connectedComponent(y).

LaTeX

$$(x : \mathrm{ConnectedComponents}(\alpha)) \neq y \iff \operatorname{connectedComponent}(x) \neq \operatorname{connectedComponent}(y)$$

Lean4

theorem coe_ne_coe {x y : α} : (x : ConnectedComponents α) ≠ y ↔ connectedComponent x ≠ connectedComponent y :=
  coe_eq_coe.not

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