comap_iff — Mathlib

English

For a linear isometry equivalence f, U.comap f ⟂ V.comap f iff U ⟂ V.

Русский

Для линейного изометрического отображения эквивалентности f, U.comap f ⟂ V.comap f ⇔ U ⟂ V.

LaTeX

$$(U.comap f \perp V.comap f) \iff (U \perp V)$$

Lean4

@[simp]
theorem comap_iff (f : E ≃ₗᵢ[𝕜] F) {U V : Submodule 𝕜 F} : U.comap f ⟂ V.comap f ↔ U ⟂ V :=
  ⟨fun h =>
    by
    have hf : ∀ p : Submodule 𝕜 F, (p.comap f).map f.toLinearIsometry = p := map_comap_eq_of_surjective f.surjective
    simpa only [hf] using h.map f.toLinearIsometry, IsOrtho.comap f.toLinearIsometry⟩

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