isLittleOTVS_prodMk_left — Mathlib

English

Left projection preserves IsLittleOTVS for a product; the pairwise component relations imply the product relation.

Русский

Левая проекция сохраняет IsLittleOTVS для произведения; отношения по компонентам в сочетании дают произведение.

LaTeX

$$$\\text{IsLittleOTVS}(l, (f,g), k) \\iff (\\text{IsLittleOTVS}(l, f, k) \\land \\text{IsLittleOTVS}(l, g, k)).$$$

Lean4

@[simp]
theorem isLittleOTVS_prodMk_left [ContinuousSMul 𝕜 E] [ContinuousSMul 𝕜 F] {k : α → G} :
    (fun x ↦ (f x, g x)) =o[𝕜; l] k ↔ f =o[𝕜; l] k ∧ g =o[𝕜; l] k :=
  ⟨fun h ↦ ⟨h.fst, h.snd⟩, fun h ↦ h.elim .prodMk⟩

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