ext_s — Mathlib

English

Two Semiquots are equal if and only if their underlying sets s are equal.

Русский

Два Semiquot равны тогда, когда совпадают их основания s.

LaTeX

$$$\forall {q_1 q_2 : Semiquot α},\ q_1 = q_2 \iff q_1.s = q_2.s$$$

Lean4

theorem ext_s {q₁ q₂ : Semiquot α} : q₁ = q₂ ↔ q₁.s = q₂.s :=
  by
  refine ⟨congr_arg _, fun h => ?_⟩
  obtain ⟨_, v₁⟩ := q₁; obtain ⟨_, v₂⟩ := q₂; congr
  exact Subsingleton.helim (congrArg Trunc (congrArg Set.Elem h)) v₁ v₂

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