sup_sInf_eq — Mathlib

English

In a Coframe, the supremum distributes over infimum: a ∨ sInf s = ⨅ b∈s, a ∨ b.

Русский

В Coframe верхняя граница распространяется на infimum: a ∨ sInf s = ∧_{b∈s} (a ∨ b).

LaTeX

$$$a \vee \bigwedge s = \bigwedge_{b \in s} (a \vee b)$$$

Lean4

/-- `⊔` distributes over `⨅`. -/
theorem sup_sInf_eq {α : Type*} [Order.Coframe α] {s : Set α} {a : α} : a ⊔ sInf s = ⨅ b ∈ s, a ⊔ b :=
  gc_sdiff_sup.u_sInf

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