inf_left_eq_bot_iff

Mathlib.Order.Disjoint

URI: https://scilib.ai/kg/mathlib#IsCompl.inf_left_eq_bot_iff

English

If y and z are complements, then x ∧ y = ⊥ iff x ≤ z.

Русский

Если y и z комплементы, то x ∧ y = ⊥ тогда и только тогда, когда x ≤ z.

LaTeX

$$$$ IsCompl(y,z) \rightarrow (x \wedge y = \bot) \iff (x \le z). $$$$

Lean4

theorem inf_left_eq_bot_iff (h : IsCompl y z) : x ⊓ y = ⊥ ↔ x ≤ z := by
  rw [← le_bot_iff, ← h.le_sup_right_iff_inf_left_le, bot_sup_eq]

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

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

Разделы

Аффилиация

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