ofIsCompl_eq' — Mathlib

English

If h is IsCompl(p,q) and φ, ψ are linear maps with χ such that φ = χ ∘ p.subtype and ψ = χ ∘ q.subtype, then the glued map equals χ.

Русский

Если h = IsCompl(p,q) и φ, ψ такие, что φ = χ ∘ p.subtype и ψ = χ ∘ q.subtype, то слитое отображение равно χ.

LaTeX

$$$φ=χ\circ p.subtype\; and\; ψ=χ\circ q.subtype\; \Rightarrow\; ofIsCompl h φ ψ = χ.$$$

Lean4

theorem ofIsCompl_eq' (h : IsCompl p q) {φ : p →ₗ[R] F} {ψ : q →ₗ[R] F} {χ : E →ₗ[R] F} (hφ : φ = χ.comp p.subtype)
    (hψ : ψ = χ.comp q.subtype) : ofIsCompl h φ ψ = χ :=
  ofIsCompl_eq h (fun _ => hφ.symm ▸ rfl) fun _ => hψ.symm ▸ rfl

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