heq_iff_coe_eq — Mathlib

English

If p x ≡ q x for all x, then HEq of subtypes a1 ≍ a2 is equivalent to Eq a1.val a2.val.

Русский

Если p и q равны постклассово, то HEq подтипов a1 ≍ a2 эквивалентно равенству значений a1.val и a2.val.

LaTeX

$$$ \\forall {a_1 a_2}, a_1 \\overset{HEq}{\\approx} a_2 \\iff (a_1 : \\alpha) = (a_2 : \\alpha) $$$

Lean4

theorem heq_iff_coe_eq (h : ∀ x, p x ↔ q x) {a1 : { x // p x }} {a2 : { x // q x }} : a1 ≍ a2 ↔ (a1 : α) = (a2 : α) :=
  Eq.rec (motive := fun (pp : (α → Prop)) _ ↦ ∀ a2' : { x // pp x }, a1 ≍ a2' ↔ (a1 : α) = (a2' : α)) (by grind)
    (funext <| fun x ↦ propext (h x)) a2

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