Commit 2023-05-26 04:47 d3d280eb

View on Github →

feat: port Analysis.InnerProductSpace.Orthogonal (#4363)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/InnerProductSpace/Orthogonal.lean

added theorem OrthogonalFamily.isOrtho

added theorem Submodule.IsOrtho.comap

added theorem Submodule.IsOrtho.comap_iff

added theorem Submodule.IsOrtho.disjoint

added theorem Submodule.IsOrtho.ge

added theorem Submodule.IsOrtho.inner_eq

added theorem Submodule.IsOrtho.le

added theorem Submodule.IsOrtho.map

added theorem Submodule.IsOrtho.map_iff

added theorem Submodule.IsOrtho.mono

added theorem Submodule.IsOrtho.mono_left

added theorem Submodule.IsOrtho.mono_right

added theorem Submodule.IsOrtho.symm

added def Submodule.IsOrtho

added theorem Submodule.bot_orthogonal_eq_top

added theorem Submodule.iInf_orthogonal

added theorem Submodule.inf_orthogonal

added theorem Submodule.inf_orthogonal_eq_bot

added theorem Submodule.inner_left_of_mem_orthogonal

added theorem Submodule.inner_right_of_mem_orthogonal

added theorem Submodule.isClosed_orthogonal

added theorem Submodule.isOrtho_bot_left

added theorem Submodule.isOrtho_bot_right

added theorem Submodule.isOrtho_comm

added theorem Submodule.isOrtho_iSup_left

added theorem Submodule.isOrtho_iSup_right

added theorem Submodule.isOrtho_iff_inner_eq

added theorem Submodule.isOrtho_iff_le

added theorem Submodule.isOrtho_orthogonal_left

added theorem Submodule.isOrtho_orthogonal_right

added theorem Submodule.isOrtho_sSup_left

added theorem Submodule.isOrtho_sSup_right

added theorem Submodule.isOrtho_self

added theorem Submodule.isOrtho_span

added theorem Submodule.isOrtho_sup_left

added theorem Submodule.isOrtho_sup_right

added theorem Submodule.isOrtho_top_left

added theorem Submodule.isOrtho_top_right

added theorem Submodule.le_orthogonal_orthogonal

added theorem Submodule.mem_orthogonal'

added theorem Submodule.mem_orthogonal

added theorem Submodule.mem_orthogonal_singleton_iff_inner_left

added theorem Submodule.mem_orthogonal_singleton_iff_inner_right

added def Submodule.orthogonal

added theorem Submodule.orthogonalFamily_self

added theorem Submodule.orthogonal_disjoint

added theorem Submodule.orthogonal_eq_inter

added theorem Submodule.orthogonal_eq_top_iff

added theorem Submodule.orthogonal_gc

added theorem Submodule.orthogonal_le

added theorem Submodule.orthogonal_orthogonal_monotone

added theorem Submodule.sInf_orthogonal

added theorem Submodule.sub_mem_orthogonal_of_inner_left

added theorem Submodule.sub_mem_orthogonal_of_inner_right

added theorem Submodule.symmetric_isOrtho

added theorem Submodule.top_orthogonal_eq_bot

added theorem bilinFormOfRealInner_orthogonal

added theorem orthogonalFamily_iff_pairwise