Documentation
Init
.
Data
.
Char
.
Lemmas
Search
return to top
source
Imports
Init.Data.Char.Basic
Init.Data.UInt.Lemmas
Imported by
Char
.
ext
Char
.
le_def
Char
.
lt_def
Char
.
lt_iff_val_lt_val
Char
.
not_le
Char
.
not_lt
Char
.
le_refl
Char
.
lt_irrefl
Char
.
le_trans
Char
.
lt_trans
Char
.
le_total
Char
.
le_antisymm
Char
.
lt_asymm
Char
.
ne_of_lt
Char
.
ltIrrefl
Char
.
leRefl
Char
.
leTrans
Char
.
ltTrans
Char
.
notLTTrans
Char
.
leAntisymm
Char
.
notLTAntisymm
Char
.
ltAsymm
Char
.
leTotal
Char
.
notLTTotal
Char
.
utf8Size_eq
Char
.
ofNat_toNat
String
.
csize
source
theorem
Char
.
ext
{a b :
Char
}
:
a
.val
=
b
.val
→
a
=
b
source
theorem
Char
.
le_def
{a b :
Char
}
:
a
≤
b
↔
a
.val
≤
b
.val
source
theorem
Char
.
lt_def
{a b :
Char
}
:
a
<
b
↔
a
.val
<
b
.val
source
theorem
Char
.
lt_iff_val_lt_val
{a b :
Char
}
:
a
<
b
↔
a
.val
<
b
.val
source
@[simp]
theorem
Char
.
not_le
{a b :
Char
}
:
¬
a
≤
b
↔
b
<
a
source
@[simp]
theorem
Char
.
not_lt
{a b :
Char
}
:
¬
a
<
b
↔
b
≤
a
source
@[simp]
theorem
Char
.
le_refl
(a :
Char
)
:
a
≤
a
source
@[simp]
theorem
Char
.
lt_irrefl
(a :
Char
)
:
¬
a
<
a
source
theorem
Char
.
le_trans
{a b c :
Char
}
:
a
≤
b
→
b
≤
c
→
a
≤
c
source
theorem
Char
.
lt_trans
{a b c :
Char
}
:
a
<
b
→
b
<
c
→
a
<
c
source
theorem
Char
.
le_total
(a b :
Char
)
:
a
≤
b
∨
b
≤
a
source
theorem
Char
.
le_antisymm
{a b :
Char
}
:
a
≤
b
→
b
≤
a
→
a
=
b
source
theorem
Char
.
lt_asymm
{a b :
Char
}
(h :
a
<
b
)
:
¬
b
<
a
source
theorem
Char
.
ne_of_lt
{a b :
Char
}
(h :
a
<
b
)
:
a
≠
b
source
instance
Char
.
ltIrrefl
:
Std.Irrefl
fun (
x1
x2
:
Char
) =>
x1
<
x2
source
instance
Char
.
leRefl
:
Std.Refl
fun (
x1
x2
:
Char
) =>
x1
≤
x2
source
instance
Char
.
leTrans
:
Trans
(fun (
x1
x2
:
Char
) =>
x1
≤
x2
)
(fun (
x1
x2
:
Char
) =>
x1
≤
x2
)
fun (
x1
x2
:
Char
) =>
x1
≤
x2
Equations
Char.leTrans
=
{
trans
:=
⋯
}
source
instance
Char
.
ltTrans
:
Trans
(fun (
x1
x2
:
Char
) =>
x1
<
x2
)
(fun (
x1
x2
:
Char
) =>
x1
<
x2
)
fun (
x1
x2
:
Char
) =>
x1
<
x2
Equations
Char.ltTrans
=
{
trans
:=
⋯
}
source
def
Char
.
notLTTrans
:
Trans
(fun (
x1
x2
:
Char
) =>
¬
x1
<
x2
)
(fun (
x1
x2
:
Char
) =>
¬
x1
<
x2
)
fun (
x1
x2
:
Char
) =>
¬
x1
<
x2
Equations
Char.notLTTrans
=
{
trans
:=
@
Char.notLTTrans.proof_1
}
Instances For
source
instance
Char
.
leAntisymm
:
Std.Antisymm
fun (
x1
x2
:
Char
) =>
x1
≤
x2
source
def
Char
.
notLTAntisymm
:
Std.Antisymm
fun (
x1
x2
:
Char
) =>
¬
x1
<
x2
Equations
Char.notLTAntisymm
=
⋯
Instances For
source
instance
Char
.
ltAsymm
:
Std.Asymm
fun (
x1
x2
:
Char
) =>
x1
<
x2
source
instance
Char
.
leTotal
:
Std.Total
fun (
x1
x2
:
Char
) =>
x1
≤
x2
source
def
Char
.
notLTTotal
:
Std.Total
fun (
x1
x2
:
Char
) =>
¬
x1
<
x2
Equations
Char.notLTTotal
=
⋯
Instances For
source
theorem
Char
.
utf8Size_eq
(c :
Char
)
:
c
.utf8Size
=
1
∨
c
.utf8Size
=
2
∨
c
.utf8Size
=
3
∨
c
.utf8Size
=
4
source
@[simp]
theorem
Char
.
ofNat_toNat
(c :
Char
)
:
Char.ofNat
c
.toNat
=
c
source
@[reducible, inline, deprecated Char.utf8Size (since := "2024-06-04")]
abbrev
String
.
csize
(c :
Char
)
:
Nat
Equations
String.csize
=
Char.utf8Size
Instances For