ne_bot_of_ne_top'

Mathlib.Order.Disjoint

URI: https://scilib.ai/kg/mathlib#Codisjoint.ne_bot_of_ne_top'

Lean4

theorem ne_bot_of_ne_top' (h : Codisjoint a b) (hb : b ≠ ⊤) : a ≠ ⊥ := by rintro rfl; exact hb <| by simpa using h

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

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

Разделы

Аффилиация

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