eq_of_chain — Mathlib

English

In a chain of Part α, if some a and some b appear, then a = b.

Русский

В цепи Part α, если встречаются some a и some b, то a = b.

LaTeX

$$$$ \forall c: \text{Chain }(\text{Part }\alpha), \; \text{if } \text{some } a \in c \text{ and } \text{some } b \in c, \text{ then } a=b. $$$$

Lean4

theorem eq_of_chain {c : Chain (Part α)} {a b : α} (ha : some a ∈ c) (hb : some b ∈ c) : a = b :=
  by
  obtain ⟨i, ha⟩ := ha; replace ha := ha.symm
  obtain ⟨j, hb⟩ := hb; replace hb := hb.symm
  rw [eq_some_iff] at ha hb
  rcases le_total i j with hij | hji
  · have := c.monotone hij _ ha; apply mem_unique this hb
  · have := c.monotone hji _ hb; apply Eq.symm; apply mem_unique this ha

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