codisjoint_inf_right — Mathlib

English

In a distributive lattice with top, Codisjoint (a ∧ b) c is equivalent to Codisjoint a c and Codisjoint b c (same as the previous variant, simplified).

Русский

В той же ситуации 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_right : Codisjoint a (b ⊓ c) ↔ Codisjoint a b ∧ Codisjoint a c := by
  simp only [codisjoint_iff, sup_inf_left, inf_eq_top_iff]

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