or_le

Mathlib.Data.Bool.Basic

URI: https://scilib.ai/kg/mathlib#Bool.or_le

English

If x ≤ z and y ≤ z then (x ∨ y) ≤ z for booleans x,y,z.

Русский

Если x ≤ z и y ≤ z, то (x ∨ y) ≤ z для булевых x,y,z.

LaTeX

$$$ \forall x,y,z : Bool,\; x \le z \rightarrow y \le z \rightarrow (x \lor y) \le z $$$

Lean4

theorem or_le : ∀ {x y z}, x ≤ z → y ≤ z → (x || y) ≤ z := by decide

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

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

Разделы

Аффилиация

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