inf_sSup_eq — Mathlib

English

In an ordered frame, the infimum of a with sSup s equals the supremum over b∈s of the infimum of a with b: a ∧ sSup s = ⨆ b∈s, a ∧ b.

Русский

В рамке порядка infimum элемента a и наибольшего верхнего предела sSup s равен наибольшему нижнему пределу элементов a ∧ b по всем b∈s.

LaTeX

$$$a \wedge \bigvee s = \bigvee_{b \in s} (a \wedge b)$$$

Lean4

/-- `⊓` distributes over `⨆`. -/
theorem inf_sSup_eq {α : Type*} [Order.Frame α] {s : Set α} {a : α} : a ⊓ sSup s = ⨆ b ∈ s, a ⊓ b :=
  gc_inf_himp.l_sSup

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