disjoint_sup_right_of_disjoint_sup_left

English

If a,b,c are elements of a lattice with a bottom, and a ⊥ b, and (a ⊔ b) ⊥ c, then a ⊥ (b ⊔ c).

Русский

Пусть элементы a,b,c лежат в решётке с нулём; если a не пересекает b и (a ⊔ b) не пересекает c, то a не пересекает (b ⊔ c).

LaTeX

$$$\text{Disjoint } a b \rightarrow \text{Disjoint } (a\vee b) c \rightarrow \text{Disjoint } a (b\vee c).$$$

Lean4

theorem disjoint_sup_right_of_disjoint_sup_left [Lattice α] [OrderBot α] [IsModularLattice α] (h : Disjoint a b)
    (hsup : Disjoint (a ⊔ b) c) : Disjoint a (b ⊔ c) :=
  by
  rw [disjoint_iff_inf_le, ← h.eq_bot, sup_comm]
  apply le_inf inf_le_left
  apply (inf_le_inf_right (c ⊔ b) le_sup_right).trans
  rw [sup_comm, IsModularLattice.sup_inf_sup_assoc, hsup.eq_bot, bot_sup_eq]

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