## Stream: maths

### Topic: New linear algebra notation

#### Heather Macbeth (Dec 30 2020 at 16:00):

I would like to introduce notation for (1) the span of a single vector, (2) the orthogonal complement. I was thinking of using 𝕜 ∙ v (that's \.) and K† (that's \dagger). So:

import analysis.normed_space.inner_product

open_locale real_inner_product_space
open submodule

notation 𝕜∙:1000 x := span 𝕜 (@singleton _ _ set.has_singleton x)
notation K†:1000 := submodule.orthogonal K

variables {E : Type*} [inner_product_space ℝ E]

example {v w : E} (hw : w ∈ (ℝ ∙ v)†) : ⟪w, v⟫ = 0 :=
inner_left_of_mem_orthogonal (mem_span_singleton_self v) hw


Any alternative suggestions, or objections, before I do this? One point is that obviously ⊥ (\bot) would have been ideal for the orthogonal complement notation, but it is already taken. Does anyone know of a visual twin?

#### Heather Macbeth (Dec 30 2020 at 16:01):

See https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Notation.20for.20span for brief previous discussion of the span notation (mostly focused on getting the notation to work).

#### Adam Topaz (Dec 30 2020 at 16:02):

is \perp the same character as \bot ?

#### Heather Macbeth (Dec 30 2020 at 16:02):

Yes, unfortunately.

#### Heather Macbeth (Dec 30 2020 at 16:13):

Actually, I just found a OCR site for unicode
https://shapecatcher.com/
which provided some visual twins for ⊥, namely ⟂ and ┴. Let me try to use one of them.

#### Adam Topaz (Dec 30 2020 at 16:15):

Oh this one is nice: Vᗮ

#### Heather Macbeth (Dec 30 2020 at 16:17):

Oh, that's perfect!

#### Adam Topaz (Dec 30 2020 at 16:18):

That's a really cool webpage btw. Similar to detexify (in case you don't know about that yet :) ) https://detexify.kirelabs.org/classify.html

#### Heather Macbeth (Dec 30 2020 at 16:19):

Yes, I found it by thinking to myself, "I need detexify for unicode!" :)

#### Heather Macbeth (Dec 30 2020 at 16:24):

So, at the moment, \perp in vscode gives the same result as \bot. Do I understand correctly that if
https://github.com/leanprover/vscode-lean/blob/master/translations.json
is edited to

"perp": "ᗮ",


then \perp would produce the new notation? Is this a kind of PR to vscode-lean that would be accepted?

Yes and yes.

#### Adam Topaz (Dec 30 2020 at 16:25):

Maybe ^perp?

#### Heather Macbeth (Dec 30 2020 at 16:26):

Maybe ^perp?

I would rather save the extra character, is your concern that some people might be used to writing \perp for \bot?

#### Adam Topaz (Dec 30 2020 at 16:27):

Yeah, but maybe everyone just uses \bot.

#### Johan Commelin (Dec 30 2020 at 16:28):

I would prefer \perp. People can get used to writing \bot quite easily, I think.

#5536 and #5538

#### Eric Wieser (Dec 30 2020 at 23:41):

Shouldn't \bot be "up tack", \perp be "perpendicular", and \^perp be the character you use?

#### Eric Wieser (Dec 30 2020 at 23:43):

("" show unicode character names)

#### Heather Macbeth (Dec 30 2020 at 23:46):

Hmm ... but personally, I like it when the vscode input is the same as the LaTeX input. I find it easier to remember.

#### Mario Carneiro (Dec 30 2020 at 23:58):

latex doesn't use unicode anyway, it has its own character naming convention

#### Heather Macbeth (Dec 31 2020 at 00:25):

Ok, more precisely, it's nice when the vscode input matches the Latex character naming convention for the corresponding mathematical symbol.

#### Eric Wieser (Dec 31 2020 at 08:39):

Wait, but isn't what I suggest above closer to latex anyway? "\perp", isn't automatically superscript: $\perp$

#### Patrick Massot (Dec 31 2020 at 09:22):

I agree with Eric actually. I think \^perp makes more sense even from a LaTeX perspective.

#### Patrick Massot (Dec 31 2020 at 09:24):

Mario Carneiro said:

latex doesn't use unicode anyway, it has its own character naming convention

You meant: "Mario doesn't use unicode in LaTeX", right? Modern LaTeX has no trouble with unicode:

\documentclass{article}

\usepackage{unicode-math}

\begin{document}
$Δ ⊥ Δ'$
\end{document}


#### Mario Carneiro (Dec 31 2020 at 09:29):

I mean that latex and unicode are independent approaches to having lots of squiggly things in text

#### Mario Carneiro (Dec 31 2020 at 09:30):

there are latex symbols that are not in unicode and vice versa

#### Heather Macbeth (Dec 31 2020 at 16:53):

I don't really mind, but let's decide before the vscode extension PR goes through.
https://github.com/leanprover/vscode-lean/pull/246

#### Heather Macbeth (Dec 31 2020 at 16:53):

/poll name for ᗮ
\perp
\^perp

#### Eric Wieser (Dec 31 2020 at 16:55):

^\perp would be cool, but it's not consistent with \^1 etc right now

#### Heather Macbeth (Dec 31 2020 at 16:55):

aagh, disregard the middle option with the typo! I can't figure out how to delete it.

#### Eric Wieser (Dec 31 2020 at 16:56):

ᗮ (canadian syllabics carrier p) at least semantically seems like a really odd choice of symbol

#### Eric Wieser (Dec 31 2020 at 17:00):

ᚆ (Ogham letter uath) suffers from the same flaw

#### Adam Topaz (Dec 31 2020 at 17:01):

V┴

#### Adam Topaz (Dec 31 2020 at 17:02):

Box drawings light up and horizontal

#### Johan Commelin (Dec 31 2020 at 17:03):

that doesn't seem too bad (-;

#### Adam Topaz (Dec 31 2020 at 17:04):

Mathjax renders $V^\perp$ as the following mathml:

<math xmlns="http://www.w3.org/1998/Math/MathML">
<msup>
<mi>V</mi>
<mo>&#x22A5;</mo>
</msup>
</math>


#### Eric Wieser (Dec 31 2020 at 17:04):

Is that $V^\perp$?

#### Adam Topaz (Dec 31 2020 at 17:04):

Yeah, V^\perp is the latex

#### Eric Wieser (Dec 31 2020 at 17:05):

Strikes me as a bug in mathjax

#### Adam Topaz (Dec 31 2020 at 17:05):

I think the <msup> tag puts the character in the superscript.

#### Eric Wieser (Dec 31 2020 at 17:07):

Right, but 22A5 is "up tack", and there's a dedicated unicode character for "perpendicular"

#### Adam Topaz (Dec 31 2020 at 17:07):

So, &#x22A5; is just the plain old \bot

#### Adam Topaz (Dec 31 2020 at 17:08):

I actually like V┴ a bit better than Vᗮ

#### Eric Wieser (Dec 31 2020 at 17:09):

I agree, 0x2534 Box drawings light up and horizontal seems like a good character to me

#### Kevin Buzzard (Dec 31 2020 at 17:10):

I actually like V┴ a bit better than Vᗮ

I might need my glasses to check whether that second one isn't just a $V^1$

#### Eric Wieser (Dec 31 2020 at 17:11):

VScode renders it for me as

image.png

#### Adam Topaz (Dec 31 2020 at 17:12):

That's reasonable imo

#### Heather Macbeth (Dec 31 2020 at 17:12):

Really? I like the small one, I think it looks more natural.

#### Heather Macbeth (Dec 31 2020 at 17:12):

https://github.com/leanprover-community/mathlib/blob/10f6c151e5abd7711c1cb06e720cc98f86234803/src/analysis/normed_space/inner_product.lean#L1715

#### Heather Macbeth (Dec 31 2020 at 17:12):

lemma submodule.inf_orthogonal (K₁ K₂ : submodule 𝕜 E) : K₁ᗮ ⊓ K₂ᗮ = (K₁ ⊔ K₂)ᗮ :=


#### Mario Carneiro (Dec 31 2020 at 17:13):

I think we already make it pretty hard to distinguish all our crazy unicode stuffs. Bigger is better

#### Kevin Buzzard (Dec 31 2020 at 17:13):

ctrl-shift-+ is usually a good replacement for when I've mislaid my glasses

#### Eric Wieser (Dec 31 2020 at 17:14):

Also what if people want to state theorems about canadian syllabics? /s

#### Adam Topaz (Dec 31 2020 at 17:15):

Here's what it looks like in my emacs:
Screenshot-from-2020-12-31-10-13-35.png

#### Heather Macbeth (Jan 01 2021 at 18:59):

\^perp is the winner. I've updated https://github.com/leanprover/vscode-lean/pull/246

#### Mario Carneiro (Jan 01 2021 at 19:00):

By the way, I voted for \^bot as well because both abbreviations can refer to the same symbol