mul — Mathlib

English

If f1 maps A into B1 and f2 maps A into B2, then the pointwise product f1 * f2 maps A into B1 * B2.

Русский

Если f1 отображает A в B1, а f2 — A в B2, то точечное произведение f1 * f2 отображает A в B1 * B2.

LaTeX

$$MapsTo f1 A B1 → MapsTo f2 A B2 → MapsTo (f1 * f2) A (B1 * B2)$$

Lean4

@[to_additive]
theorem mul [Mul β] {A : Set α} {B₁ B₂ : Set β} {f₁ f₂ : α → β} (h₁ : MapsTo f₁ A B₁) (h₂ : MapsTo f₂ A B₂) :
    MapsTo (f₁ * f₂) A (B₁ * B₂) := fun _ h => mul_mem_mul (h₁ h) (h₂ h)

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