smul_set_pi_of_surjective — Mathlib

English

Let c act on a family s(i) indexed by I, with surjectivity outside I; then c · I.pi s = I.pi (c · s)

Русский

Пусть c действует на семейство множеств s(i), индексируемое I; при этом вне I отображение сюръективно; тогда c · I.pi s = I.pi (c · s)

LaTeX

$$$ c \\cdot (I \\mapsto s) = I \\mapsto (c \\cdot s) \\quad \\text{provided} \\; \\forall i \\notin I,\\; \\text{Surjective}(c \\cdot -) \\text{ на } \\pi_i $$$

Lean4

@[to_additive]
theorem smul_set_pi_of_surjective (c : M) (I : Set ι) (s : ∀ i, Set (π i))
    (hsurj : ∀ i ∉ I, Function.Surjective (c • · : π i → π i)) : c • I.pi s = I.pi (c • s) :=
  piMap_image_pi hsurj s

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