Commit 2026-01-17 20:29 1839d10b

View on Github →

feat(Analysis/InnerProductSpace/Orthogonal): add duplicates for ClosedSubmodule (#29241) add duplicates of definitions and API's for ClosedSubmodule in an InnerProductSpace. motivation: when one considers a Hilbert space (CompleteSpace), it is more natural to consider ClosedSubmodules. They form a complete lattice and satisfy sup_orthogonal #29243.

depends on: #29230 for Lattice CompleteLattice

Estimated changes

Modified Mathlib/Analysis/Convex/Cone/Basic.lean

modified theorem ProperCone.mem_toPointedCone

Modified Mathlib/Analysis/InnerProductSpace/Orthogonal.lean

added theorem ClosedSubmodule.bot_orthogonal_eq_top

added theorem ClosedSubmodule.iInf_orthogonal

added theorem ClosedSubmodule.inf_orthogonal

added theorem ClosedSubmodule.inf_orthogonal_eq_bot

added theorem ClosedSubmodule.mem_orthogonal'

added theorem ClosedSubmodule.mem_orthogonal

added theorem ClosedSubmodule.mem_orthogonal_iff

added def ClosedSubmodule.orthogonal

added theorem ClosedSubmodule.orthogonal_closure''

added theorem ClosedSubmodule.orthogonal_closure'

added theorem ClosedSubmodule.orthogonal_closure

added theorem ClosedSubmodule.orthogonal_disjoint

added theorem ClosedSubmodule.orthogonal_eq_inter

added theorem ClosedSubmodule.orthogonal_eq_top_iff

added theorem ClosedSubmodule.orthogonal_gc

added theorem ClosedSubmodule.orthogonal_le

added theorem ClosedSubmodule.orthogonal_orthogonal_monotone

added theorem ClosedSubmodule.orthogonal_toSubmodule_eq

added theorem ClosedSubmodule.sInf_orthogonal

added theorem ClosedSubmodule.sub_mem_orthogonal_of_inner_left

added theorem ClosedSubmodule.sub_mem_orthogonal_of_inner_right

added theorem ClosedSubmodule.top_orthogonal_eq_bot

added theorem Submodule.orthogonal_closure'

Modified Mathlib/Topology/Algebra/Module/ClosedSubmodule.lean

added theorem ClosedSubmodule.mem_toSubmodule_iff

added theorem Submodule.closure_eq'

added theorem Submodule.closure_eq