isCompl_iff — Mathlib

English

In a partial order with a top and bottom, IsCompl a b holds if and only if both Disjoint a b and Codisjoint a b hold.

Русский

При частичном порядке с максимумом и минимумом IsCompl a b эквивалентно тому, что одновременно верны Disjoint a b и Codisjoint a b.

LaTeX

$$$\text{IsCompl}(a,b) \iff (\text{Disjoint}(a,b) \land \text{Codisjoint}(a,b))$$$

Lean4

theorem isCompl_iff [PartialOrder α] [BoundedOrder α] {a b : α} : IsCompl a b ↔ Disjoint a b ∧ Codisjoint a b :=
  ⟨fun h ↦ ⟨h.1, h.2⟩, fun h ↦ ⟨h.1, h.2⟩⟩

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