exists_inf_le — Mathlib

English

Let f : α → β with β a SemilatticeInf, an OrderTop, and WellFoundedLT. There exists a finite t ⊆ α such that for all a, t.inf f ≤ f(a).

Русский

Пусть f: α → β, β является полуустановленной полемой инфимумной решёткой с верхней границей и хорошо упорядоченным отношением «меньше чем»; существует конечное подмножество t ⊆ α такое, что для всех a выполнено t.inf f ≤ f(a).

LaTeX

$$$\exists t : Finset\, \alpha, \forall a, t.inf f \le f(a)$$$

Lean4

theorem exists_inf_le [SemilatticeInf β] [OrderTop β] [WellFoundedLT β] (f : α → β) :
    ∃ t : Finset α, ∀ a, t.inf f ≤ f a :=
  exists_sup_ge (β := βᵒᵈ) _

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