coe_eq_coe' — Mathlib

English

The equality (x : ConnectedComponents α) = y is equivalent to x ∈ connectedComponent(y).

Русский

Равенство (x : ConnectedComponents α) = y эквивалентно x ∈ connectedComponent(y).

LaTeX

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

Lean4

theorem coe_eq_coe' {x y : α} : (x : ConnectedComponents α) = y ↔ x ∈ connectedComponent y :=
  coe_eq_coe.trans connectedComponent_eq_iff_mem

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