coe_sSup — Mathlib

English

A convenient form of coe_sSup: the coercion of sSup s equals the supremum of the coerced elements over s.

Русский

Удобная форма coe_sSup: приводя к элементам через включение, равно верхней грани образованной образом.

LaTeX

$$$\uparrow (sSup(s)) = \bigl( \bigsqcup_{a \in s} \uparrow a \bigr) : WithTop\, \alpha$$$

Lean4

/-- A version of `WithTop.coe_sSup'` with a more convenient but less general statement. -/
@[norm_cast]
theorem coe_sSup {s : Set α} (hb : BddAbove s) : ↑(sSup s) = (⨆ a ∈ s, ↑a : WithTop α) := by
  rw [coe_sSup' hb, sSup_image]

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