mk_smul_of_tower_mk — Mathlib

English

For any s ∈ SetLike S α closed under the tower, r•(⟨x, hx⟩) equals ⟨r•x, proof⟩ in the subtype.

Русский

Для любого s ∈ SetLike S α, замкнутого относительно башни, действие на элемент⟨x, hx⟩ даёт ⟨r•x, доказательство⟩ в подтипе.

LaTeX

$$$r \\cdot (⟨x, hx⟩) = ⟨r \\cdot x, smul\\_mem\\_\\_ hx⟩$$$

Lean4

@[to_additive (attr := simp)]
theorem mk_smul_of_tower_mk (r : M) (x : α) (hx : x ∈ s) :
    r • (⟨x, hx⟩ : s) = ⟨r • x, smul_one_smul N r x ▸ smul_mem _ hx⟩ :=
  rfl

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