Zulip Chat Archive

Stream: new members

Topic: introducing a weird less-than symbol


view this post on Zulip Michael Beeson (Jan 01 2021 at 00:56):

I need two kinds of less-than, so I have to introduce a new symbol for one of them, and I tried to make it \le\H where \H produces H in mathbb. So I made a typographical error that Reid Barton pointed out, and would delete this
post except I was told not to delete posts as they might still be useful. Thanks Reid. The example below is
fixed now.

reserve infix `  `: 49
reserve infix ` < `: 49

class  Model (M:Type) :=
(𝔽:M)
(𝕊:M  M)  --successor
(zero:M)
(mem:M  M  Prop)
(addition: M  M  M)
(le: M  M  Prop)
(leH: M  M  Prop)
(lessthan: M  M  Prop)
(lessthanH: M  M  Prop)
(infix   :=  mem )
(infix  + := addition)
(additive_identity:  x, x  𝔽   x + zero = x)
(leH_definition:  x y, (leH x y   k, x + k = y))
(lessthanH_definition:  x y, (lessthanH x y   k, x + 𝕊 k = y))

variables (M:Type) [Model M] (a b x y z u v w X R W: M)

open Model
infix + := addition
infix   := leH
infix  < := lessthanH

lemma test3:  (x:M), x + zero  x:=
  begin

  end

view this post on Zulip Reid Barton (Jan 01 2021 at 00:59):

I think you wanted to define infix <ℍ := lessthanH


Last updated: May 13 2021 at 06:15 UTC