sSup_inf_eq — Mathlib

English

Let s be a directed subset of a complete lattice α that is compactly generated. Then the meet of the supremum of s with a equals the supremum of all pairwise meets with a: (sup s) ∧ a = sup { b ∧ a : b ∈ s }.

Русский

Пусть s — направленный подмножество в полной решётке α, которая является компактно порождаемой. Тогдаmeet( sup s, a ) равно sup( { b ∧ a : b ∈ s } ).

LaTeX

$$$\left(\sup s\right) \wedge a = \bigvee_{b \in s} (b \wedge a)$$$

Lean4

/-- This property is sometimes referred to as `α` being upper continuous. -/
protected theorem sSup_inf_eq (h : DirectedOn (· ≤ ·) s) : sSup s ⊓ a = ⨆ b ∈ s, b ⊓ a := by
  simp_rw [inf_comm _ a, h.inf_sSup_eq]

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