ofIsComplProd_apply — Mathlib

English

Applying the composed projection to a pair (a,b) in the product recovers the projected pair (φ a, ψ b).

Русский

Применение полученной проекции к паре (a,b) восстанавливает пару (φ a, ψ b).

LaTeX

$$$\mathrm{ofIsComplProd}\ h\; φ\; ψ\; (a,b) = (φ(a), ψ(b)).$$$

Lean4

@[simp]
theorem ofIsComplProd_apply {p q : Submodule R₁ E} (h : IsCompl p q) (φ : (p →ₗ[R₁] F) × (q →ₗ[R₁] F)) :
    ofIsComplProd h φ = ofIsCompl h φ.1 φ.2 :=
  rfl

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