inf_iInf_nat_succ — Mathlib

English

For a sequence u: ℕ → α, the meet of u(0) with the infimum over i of u(i+1) equals the infimum over i of u(i): u(0) ∧ (inf_{i} u(i+1)) = inf_{i} u(i).

Русский

Для последовательности u: ℕ → α, пересечение u(0) с инфиминумом над i+1 даёт инфиминум последовательности: u(0) ∧ (inf_{i} u(i+1)) = inf_{i} u(i).

LaTeX

$$$u(0) \land \Bigl(\inf_{i} u(i+1)\Bigr) = \inf_{i} u(i)$$$

Lean4

theorem inf_iInf_nat_succ (u : ℕ → α) : (u 0 ⊓ ⨅ i, u (i + 1)) = ⨅ i, u i :=
  @sup_iSup_nat_succ αᵒᵈ _ u

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