smul_iSup — Mathlib

English

For T and S_i as above, the equality (T • ⨆ i, S_i) = ⨆ i, T • S_i holds.

Русский

Справедливо (T • ⨆ i, S_i) = ⨆ i, T • S_i.

LaTeX

$$$T \cdot \left( \bigsqcup_i S_i \right) = \bigsqcup_i (T \cdot S_i)$$$

Lean4

theorem smul_iSup (T : AddSubmonoid R) (S : ι → AddSubmonoid A) : (T • ⨆ i, S i) = ⨆ i, T • S i :=
  le_antisymm
    (smul_le.mpr fun t ht s hs ↦
      iSup_induction _ (motive := (t • · ∈ _)) hs (fun i s hs ↦ mem_iSup_of_mem i <| smul_mem_smul ht hs)
        (by simp_rw [smul_zero]; apply zero_mem) fun x y ↦ by simp_rw [smul_add]; apply add_mem)
    (iSup_le fun i ↦ smul_le_smul_right <| le_iSup _ i)

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