exists_inf_eq_iInf — Mathlib

English

For a function f: α → β with β a complete lattice and WellFoundedLT, there exists t : Finset α such that t.inf f = ⨅ a, f a.

Русский

Для функции f: α → β в полной решётке β, существует конечный набор t ⊆ α такой, что ∧_{x∈t} f(x) равно инфимума над всеми a: f(a).

LaTeX

$$$\exists t : Finset\, \alpha, \ t.inf f = \bigwedge_{a: \alpha} f(a)$$$

Lean4

theorem exists_inf_eq_iInf [CompleteLattice β] [WellFoundedLT β] (f : α → β) : ∃ t : Finset α, t.inf f = ⨅ a, f a :=
  exists_sup_eq_iSup (β := βᵒᵈ) _

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