coe_sSup — Mathlib

English

If a ≤ b and S is a nonempty set of elements of Set.Icc a b, then coercion commutes with supremum: the coe of sSup S equals the supremum of the coercions.

Русский

Если a ≤ b и S — непустое множество элементов Set.Icc a b, то вложение в α commute с supremum: коe(sSup S) = sSup(coe''S).

LaTeX

$$$$ x \le y \Rightarrow \uparrow(\operatorname{sSup} S) = \operatorname{sSup}(\uparrow\!''S) $$$$

Lean4

theorem coe_sSup [ConditionallyCompleteLattice α] {a b : α} (h : a ≤ b) {S : Set (Set.Icc a b)} (hS : S.Nonempty) :
    have : Fact (a ≤ b) := ⟨h⟩
    ↑(sSup S) = sSup ((↑) '' S : Set α) :=
  congrArg Subtype.val (dif_neg hS.ne_empty)

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