Commit 2020-12-31 10:07 10f6c151

View on Github →

chore(analysis/normed_space/inner_product): notation for orthogonal complement (#5536) Notation for submodule.orthogonal, so that one can write Kᗮ instead of K.orthogonal. Simultaneous PR https://github.com/leanprover/vscode-lean/pull/246 adds \perp as vscode shorthand for this symbol. Zulip

Estimated changes

Modified src/analysis/normed_space/dual.lean

Modified src/analysis/normed_space/inner_product.lean

modified theorem orthogonal_eq_inter

modified theorem submodule.Inf_orthogonal

modified theorem submodule.bot_orthogonal_eq_top

modified theorem submodule.inf_orthogonal

modified theorem submodule.infi_orthogonal

modified theorem submodule.is_closed_orthogonal

modified theorem submodule.le_orthogonal_orthogonal

modified theorem submodule.mem_orthogonal'

modified theorem submodule.mem_orthogonal

modified theorem submodule.orthogonal_disjoint

modified theorem submodule.orthogonal_le

modified theorem submodule.orthogonal_orthogonal

modified theorem submodule.top_orthogonal_eq_bot

Modified src/geometry/euclidean/basic.lean

Modified src/geometry/euclidean/monge_point.lean