coe_eq_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)) = y \iff \operatorname{connectedComponent}(x) = \operatorname{connectedComponent}(y)$$

Lean4

@[simp]
theorem coe_eq_coe {x y : α} : (x : ConnectedComponents α) = y ↔ connectedComponent x = connectedComponent y :=
  Quotient.eq''

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