le_and

Mathlib.Data.Bool.Basic

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

English

For booleans x, y, z, if x ≤ y and x ≤ z, then x ≤ (y ∧ z).

Русский

Для булевых x,y,z: если x ≤ y и x ≤ z, то x ≤ (y ∧ z).

LaTeX

$$$ \forall {x,y,z : Bool},\; x \le y \rightarrow x \le z \rightarrow x \le (y \land z) $$$

Lean4

theorem le_and : ∀ {x y z : Bool}, x ≤ y → x ≤ z → x ≤ (y && z) := by decide

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

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

Разделы

Аффилиация

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