inf_of_mem — Mathlib

English

For a nonempty finite set s and a function f : β → α into a semilattice with infimum, the infimum of f over s exists as an element a ∈ α; i.e., there is a such that inf_{b∈s} f(b) = a.

Русский

Для непустого конечного множества s и функции f: β → α в полукольце с инфимумом существующий инфимум f над s равен некоторому элементу a ∈ α; существует a = inf_{b∈s} f(b).

LaTeX

$$$\\exists a \\in α, \\; \\inf_{b\\in s} f(b) = a$$$

Lean4

theorem inf_of_mem {s : Finset β} (f : β → α) {b : β} (h : b ∈ s) : ∃ a : α, s.inf ((↑) ∘ f : β → WithTop α) = ↑a :=
  @sup_of_mem αᵒᵈ _ _ _ f _ h

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