coe_sInf — Mathlib

English

A convenient form of coe_sInf: the coercion of sInf s equals the infimum of the coerced elements over s.

Русский

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

LaTeX

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

Lean4

/-- A version of `WithTop.coe_sInf'` with a more convenient but less general statement. -/
@[norm_cast]
theorem coe_sInf {s : Set α} (hs : s.Nonempty) (h's : BddBelow s) : ↑(sInf s) = (⨅ a ∈ s, ↑a : WithTop α) := by
  rw [coe_sInf' hs h's, sInf_image]

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