instLocallyFiniteOrderBot — Mathlib

English

For b : ∀ i, α i, the product of the Iic intervals has cardinal equal to the product of the coordinatewise Iic sizes: #(Iic b) = ∏ i #(Iic(b i)).

Русский

Для b : ∀ i, α(i) выполнено: #(Iic b) = ∏ i #(Iic(b i)).

LaTeX

$$$$ #(Iic(b)) = \\prod_{i} #(Iic(b(i))) $$$$

Lean4

instance instLocallyFiniteOrderBot : LocallyFiniteOrderBot (∀ i, α i) :=
  .ofIic _ (fun b => piFinset fun i => Iic (b i)) fun b x => by simp_rw [mem_piFinset, mem_Iic, le_def]

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