coe_inf' — Mathlib

English

Coercing the infimum from α to WithTop α preserves the infimum, i.e., the image of the infimum under the canonical embedding equals the infimum in WithTop of the composed function.

Русский

Сохранение инфимума при отображении α в WithTop α: инфимума через f, затем вводим в WithTop равно инфимума через f в WithTop.

LaTeX

$$$\\big( \\inf'_{H} f \\big)^{\\uparrow} = \\inf'_{H} (\\uparrow \\circ f)$$$

Lean4

@[simp]
theorem coe_inf' : ((s.inf' H f : α) : WithTop α) = s.inf ((↑) ∘ f) :=
  @coe_sup' αᵒᵈ _ _ _ H f

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