coe_sInf' — Mathlib

English

Coe of the infimum for WithBot α aligns with the infimum in the dual embedding of α.

Русский

Приведение инфимума для WithBot α совпадает с инфимума в двойственном вложении α.

LaTeX

$$$$ \operatorname{coe\_sInf'} \ (\text{…}) $$$$

Lean4

@[norm_cast]
theorem coe_sInf' [InfSet α] {s : Set α} (hs : BddBelow s) : ↑(sInf s) = (sInf ((fun (a : α) ↦ ↑a) '' s) : WithBot α) :=
  WithTop.coe_sSup' (α := αᵒᵈ) hs

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