inf_le_ite

Mathlib.Order.Lattice

URI: https://scilib.ai/kg/mathlib#inf_le_ite

English

For any s,s' and a decidable proposition P, s ⊓ s' ≤ ite P s s'.

Русский

Для любых s, s' иDecidable P: s ⊓ s' ≤ ite P s s'.

LaTeX

$$$ \forall s,s' \in \alpha,\ (P) [Decidable P] \Rightarrow s \wedge s' \le \operatorname{ite}(P)\ s\ s' $$$

Lean4

theorem inf_le_ite (s s' : α) (P : Prop) [Decidable P] : s ⊓ s' ≤ ite P s s' :=
  @ite_le_sup αᵒᵈ _ _ _ _ _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru