countable_biInf_eq_iInf_seq — Mathlib

English

In a complete lattice, a countable family of indices B yields a representation of the biinfimum of a family f(t) over t in B as an infimum over a sequence x(i).

Русский

В полной решётке, счетная множество индексов B задаёт представление биинфима f(t) по T как инфимум по последовательности x(i).

LaTeX

$$$$\\exists x: \\mathbb N \\to ι, \\ \\bigwedge t\\in B, f(t) = \\bigwedge_i f(x(i)).$$$$

Lean4

theorem countable_biInf_eq_iInf_seq [CompleteLattice α] {B : Set ι} (Bcbl : B.Countable) (Bne : B.Nonempty)
    (f : ι → α) : ∃ x : ℕ → ι, ⨅ t ∈ B, f t = ⨅ i, f (x i) :=
  let ⟨g, hg⟩ := Bcbl.exists_eq_range Bne
  ⟨g, hg.symm ▸ iInf_range⟩

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