codisjoint_inf_left — Mathlib

English

In a distributive lattice with top, Codisjoint (a ∧ b) c is equivalent to Codisjoint a c and Codisjoint b c.

Русский

В дистрибутивной решётке с верхом Codisjoint (a ∧ b) c эквивалентно Codisjoint a c и Codisjoint b c.

LaTeX

$$$Codisjoint (a \wedge b) c \iff Codisjoint a c \land Codisjoint b c$$$

Lean4

@[simp]
theorem codisjoint_inf_left : Codisjoint (a ⊓ b) c ↔ Codisjoint a c ∧ Codisjoint b c := by
  simp only [codisjoint_iff, sup_inf_right, inf_eq_top_iff]

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