HepLean Documentation
Init
.
Data
.
String
.
Lemmas
Search
Google site search
return to top
source
Imports
Init.Data.Char.Lemmas
Imported by
String
.
data_eq_of_eq
String
.
ne_of_data_ne
String
.
lt_irrefl
String
.
ne_of_lt
source
theorem
String
.
data_eq_of_eq
{a b :
String
}
(h :
a
=
b
)
:
a
.data
=
b
.data
source
theorem
String
.
ne_of_data_ne
{a b :
String
}
(h :
a
.data
≠
b
.data
)
:
a
≠
b
source
@[simp]
theorem
String
.
lt_irrefl
(s :
String
)
:
¬
s
<
s
source
theorem
String
.
ne_of_lt
{a b :
String
}
(h :
a
<
b
)
:
a
≠
b