English
For a family of AddSubmonoids S: ι → AddSubmonoid R and a fixed T, the product distributes over iSup: (⨆ i, S i) * T = ⨆ i, S i * T.
Русский
Для семейства аддитивных подподмножеств S: ι → AddSubmonoid R и фиксированного T выполняется распределение по iSup: (⨆ i, S i) * T = ⨆ i, S i * T.
LaTeX
$$$ \Big( \bigsqcup_{i} S_i \Big) * T = \bigsqcup_{i} (S_i * T) $$$
Lean4
theorem iSup_mul (S : ι → AddSubmonoid R) (T : AddSubmonoid R) : (⨆ i, S i) * T = ⨆ i, S i * T :=
le_antisymm
(mul_le.mpr fun s hs t ht ↦
iSup_induction _ (motive := (· * t ∈ _)) hs (fun i s hs ↦ mem_iSup_of_mem i <| mul_mem_mul hs ht)
(by simp_rw [zero_mul]; apply zero_mem) fun _ _ ↦ by simp_rw [right_distrib]; apply add_mem) <|
iSup_le fun i ↦ mul_le_mul_left (le_iSup _ i)
