add_ciSup — Mathlib

English

For f: I → Card, g: J → Card with Nonempty I,J and bounded ranges, sup_i f_i + sup_j g_j = sup_{i,j} (f_i + g_j).

Русский

Для двух семей кардиналов f_i и g_j, индексируемых непустыми множествами I,J и ограниченных сверху, выполняется (sup_i f_i) + (sup_j g_j) = sup_{i,j} (f_i + g_j).

LaTeX

$$$\forall f:I\to \mathrm{Cardinal}, \forall g:J\to \mathrm{Cardinal},\ (\sup_i f_i) + (\sup_j g_j) = \sup_{i,j} (f_i + g_j)$, при условиях связанные с не пустыми индексами и граниченностью.$$

Lean4

protected theorem add_ciSup (hf : BddAbove (range f)) (c : Cardinal.{v}) : c + (⨆ i, f i) = ⨆ i, c + f i := by
  rw [add_comm, Cardinal.ciSup_add f hf]; simp_rw [add_comm]

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