compl_anti

Mathlib.Order.Heyting.Basic

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

English

If a ≤ b, then bᶜ ≤ aᶜ.

Русский

Если a ≤ b, то bᶜ ≤ aᶜ.

LaTeX

$$If $a \le b$, then $b^{\complement} \le a^{\complement}$$$

Lean4

theorem compl_anti : Antitone (compl : α → α) := fun _ _ h => le_compl_comm.1 <| h.trans le_compl_compl

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

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

Разделы

Аффилиация

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