heq_iff_coe_heq — Mathlib

English

If a and b are subtypes with possibly different ambient types, then HEq a b is equivalent to HEq their values when α=β and p≍q.

Русский

Если a и b — подтипы с возможно различными окружающими типами, то HEq a b эквивалентно HEq их значений при равенстве базовых типов и совместимости условий.

LaTeX

$$∀ {α β} {p q}, HEq a b ↔ HEq a.val b.val$$

Lean4

theorem heq_iff_coe_heq {α β : Sort _} {p : α → Prop} {q : β → Prop} {a : { x // p x }} {b : { y // q y }} (h : α = β)
    (h' : p ≍ q) : a ≍ b ↔ (a : α) ≍ (b : β) := by
  subst h
  subst h'
  grind

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