countable_biInf_eq_iInf_seq' — Mathlib

English

If the base contains top, similar to the previous lemma, with f(t0) = ⊤, there exists a sequence x such that iInf over B equals iInf over x.

Русский

Если базис содержит ⊤ и аналогично предыдущей лемме, существует последовательность x, такая что iInf по B равен iInf по x.

LaTeX

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

Lean4

theorem countable_biInf_eq_iInf_seq' [CompleteLattice α] {B : Set ι} (Bcbl : B.Countable) (f : ι → α) {i₀ : ι}
    (h : f i₀ = ⊤) : ∃ x : ℕ → ι, ⨅ t ∈ B, f t = ⨅ i, f (x i) :=
  by
  rcases B.eq_empty_or_nonempty with hB | Bnonempty
  · rw [hB, iInf_emptyset]
    use fun _ => i₀
    simp [h]
  · exact countable_biInf_eq_iInf_seq Bcbl Bnonempty f

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