ite_le_sup — Mathlib

English

For any s, s' in a semilattice and any proposition P with decidable truth, the conditional ite P s s' is below the join s ⊔ s'.

Русский

Для любых s, s' в полулинейном пространстве и любой произвольной пропозиции P с разрешимостью, выражение if P then s else s' лежит ниже верхнего предела s ⊔ s'.

LaTeX

$$$ \forall s,s'\in\alpha,\; (P:\Prop)\; [Decidable P] \;:\ ite P\ s\ s' \le s \sqcup s' $$$

Lean4

theorem ite_le_sup (s s' : α) (P : Prop) [Decidable P] : ite P s s' ≤ s ⊔ s' :=
  if h : P then (if_pos h).trans_le le_sup_left else (if_neg h).trans_le le_sup_right

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