true_eq_false_eq_False

Mathlib.Data.Bool.Basic

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

English

True and False are distinct; in particular, true is not equal to false.

Русский

Истина и ложь различны; в частности, true не равно false.

LaTeX

$$$$ \neg(\mathrm{True} = \mathrm{False}). $$$$

Lean4

theorem true_eq_false_eq_False : ¬(true = false) := by decide

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

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

Разделы

Аффилиация

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