## Stream: new members

### Topic: introducing a weird less-than symbol

#### 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 )
(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  ≤ℍ := leH
infix  <ℍ := lessthanH

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

end


#### 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