subtypeVal_coe — Mathlib

English

The underlying function of subtypeVal is exactly the Subtype.val function.

Русский

Базовая функция subtypeVal совпадает с Subtype.val.

LaTeX

$$$\\mathrm{coe}(\\mathrm{subtypeVal}) = \\mathrm{Subtype.val}$$$

Lean4

@[simp]
theorem subtypeVal_coe {P : β → Prop} (Pbot : P ⊥) (Ptop : P ⊤) (Psup : ∀ ⦃x y⦄, P x → P y → P (x ⊔ y))
    (Pinf : ∀ ⦃x y⦄, P x → P y → P (x ⊓ y)) : ⇑(subtypeVal Pbot Ptop Psup Pinf) = Subtype.val :=
  rfl

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