congr — Mathlib

English

If a cycle s is subsingleton, then any two elements of s are equal.

Русский

Если цикл s одиночный, то любые два элемента s равны.

LaTeX

$$$\text{If } s \text{ is Subsingleton, then } \forall x,y \in s, x = y.$$$

Lean4

theorem congr {s : Cycle α} (h : Subsingleton s) : ∀ ⦃x⦄ (_hx : x ∈ s) ⦃y⦄ (_hy : y ∈ s), x = y :=
  by
  induction s using Quot.inductionOn with
  | _ l
  simp only [length_subsingleton_iff, length_coe, mk_eq_coe, le_iff_lt_or_eq, Nat.lt_add_one_iff, length_eq_zero_iff,
    length_eq_one_iff, Nat.not_lt_zero, false_or] at h
  rcases h with (rfl | ⟨z, rfl⟩) <;> simp

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