English
For f:I→Cardinal and g:J→Cardinal, (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
$$$\bigl(\sup_i f_i\bigr) \cdot \bigl(\sup_j g_j\bigr) = \sup_{i,j} (f_i \cdot g_j)$$$
Lean4
protected theorem ciSup_mul (c : Cardinal.{v}) : (⨆ i, f i) * c = ⨆ i, f i * c :=
by
cases isEmpty_or_nonempty ι; · simp
obtain rfl | h0 := eq_or_ne c 0; · simp
by_cases hf : BddAbove (range f); swap
· have hfc : ¬BddAbove (range (f · * c)) := fun bdd ↦
hf ⟨⨆ i, f i * c, forall_mem_range.mpr fun i ↦ (le_mul_right h0).trans (le_ciSup bdd i)⟩
simp [iSup, csSup_of_not_bddAbove, hf, hfc]
have : ∀ i, f i * c ≤ (⨆ i, f i) * c := fun i ↦ mul_le_mul_right' (le_ciSup hf i) c
refine le_antisymm ?_ (ciSup_le' this)
have bdd : BddAbove (range (f · * c)) := ⟨_, forall_mem_range.mpr this⟩
obtain hs | hs := lt_or_ge (⨆ i, f i) ℵ₀
· obtain ⟨i, hi⟩ := exists_eq_of_iSup_eq_of_not_isSuccLimit f hf (not_isSuccLimit_of_lt_aleph0 hs) rfl
exact hi ▸ le_ciSup bdd i
rw [mul_eq_max_of_aleph0_le_left hs h0, max_le_iff]
obtain ⟨i, hi⟩ := exists_lt_of_lt_ciSup' (one_lt_aleph0.trans_le hs)
exact ⟨ciSup_mono bdd fun i ↦ le_mul_right h0, (le_mul_left (zero_lt_one.trans hi).ne').trans (le_ciSup bdd i)⟩
