compl_inf — Mathlib

English

Let A be a Boolean algebra. Then for any x and y in A, the complement distributes over inf: (x ∧ y)^c = x^c ∨ y^c.

Русский

Пусть A — булова алгебра. Тогда для любых x, y ∈ A выполняется распределение дополнения над операцией meet: (x ∧ y)^c = x^c ∨ y^c.

LaTeX

$$$(x \wedge y)^{c} = x^{c} \vee y^{c}$$$

Lean4

@[simp]
theorem compl_inf : (x ⊓ y)ᶜ = xᶜ ⊔ yᶜ :=
  hnot_inf_distrib _ _

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