set_smul_eq_iSup — Mathlib

English

Another presentation of the set smul as an iSup over a family of submodules indexed by elements of the set.

Русский

Еще одна формулировка: s • N как iSup по семейству подмодулей с индексами по элементам множества.

LaTeX

$$$s \\cdot N = iSup (\\lambda a, a \\cdot N)$$$

Lean4

theorem set_smul_eq_iSup [SMulCommClass S R M] (s : Set S) (N : Submodule R M) : s • N = ⨆ (a ∈ s), a • N :=
  by
  refine Eq.trans (congrArg sInf ?_) csInf_Ici
  simp_rw [← Set.Ici_def, iSup_le_iff, @forall_comm M]
  exact Set.ext fun _ => forall₂_congr (fun _ _ => Iff.symm map_le_iff_le_comap)

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