subtypeVal_apply — Mathlib

English

For x in the subtype, subtypeVal maps x to itself (as an element of β).

Русский

Для x из подтипа subtypeVal отображает x в себя (как элемент β).

LaTeX

$$$\\mathrm{subtypeVal}\\;P\\;bot\\;top\\;sup\\;inf\\; x = x$$$

Lean4

@[simp]
theorem subtypeVal_apply {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)) (x : { x : β // P x }) : subtypeVal Pbot Ptop Psup Pinf x = x :=
  rfl

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