map_iff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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