AsciiCasing

📁 Source: Batteries/Data/Char/AsciiCasing.lean

Statistics

Metric	Count
Definitions beqCaseInsensitiveAsciiOnly, isSetoid, caseFoldAsciiOnly, cmpCaseInsensitiveAsciiOnly	4
Theorems eqv, isAlpha_toLower_eq_isAlpha, isAlpha_toUpper_eq_isAlpha, isLower_toLower_eq_isAlpha, isLower_toUpper_eq_false, isUpper_toLower_eq_false, isUpper_toUpper_eq_isAlpha, not_isLower_of_isUpper, not_isUpper_of_isLower, toLower_eq_of_isUpper, toLower_eq_of_not_isUpper, toLower_toLower_eq_toLower, toLower_toUpper_eq_toLower, toUpper_eq_of_isLower, toUpper_eq_of_not_isLower, toUpper_toLower_eq_toUpper, toUpper_toUpper_eq_toUpper	17
Total	21

Char

Definitions

Name	Category	Theorems
beqCaseInsensitiveAsciiOnly 📖	CompOp	1 math math: beqCaseInsensitiveAsciiOnly.eqv
caseFoldAsciiOnly 📖	CompOp	—
cmpCaseInsensitiveAsciiOnly 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isAlpha_toLower_eq_isAlpha 📖	—	—	—	—	isUpper_toLower_eq_false isLower_toLower_eq_isAlpha
isAlpha_toUpper_eq_isAlpha 📖	—	—	—	—	isUpper_toUpper_eq_isAlpha isLower_toUpper_eq_false
isLower_toLower_eq_isAlpha 📖	—	—	—	—	toLower_eq_of_isUpper toNat_ofNat toLower_eq_of_not_isUpper
isLower_toUpper_eq_false 📖	—	—	—	—	—
isUpper_toLower_eq_false 📖	—	—	—	—	—
isUpper_toUpper_eq_isAlpha 📖	—	—	—	—	toUpper_eq_of_isLower toNat_ofNat toUpper_eq_of_not_isLower
not_isLower_of_isUpper 📖	—	—	—	—	—
not_isUpper_of_isLower 📖	—	—	—	—	—
toLower_eq_of_isUpper 📖	—	—	—	—	val_ofNat ofNat_toNat_eq_val
toLower_eq_of_not_isUpper 📖	—	—	—	—	—
toLower_toLower_eq_toLower 📖	—	—	—	—	toLower_eq_of_not_isUpper isUpper_toLower_eq_false
toLower_toUpper_eq_toLower 📖	—	—	—	—	not_isUpper_of_isLower isUpper_toUpper_eq_isAlpha toLower_eq_of_isUpper toUpper_eq_of_isLower toLower_eq_of_not_isUpper toNat_ofNat toUpper_eq_of_not_isLower
toUpper_eq_of_isLower 📖	—	—	—	—	val_ofNat ofNat_toNat_eq_val
toUpper_eq_of_not_isLower 📖	—	—	—	—	—
toUpper_toLower_eq_toUpper 📖	—	—	—	—	not_isLower_of_isUpper isLower_toLower_eq_isAlpha toUpper_eq_of_isLower toLower_eq_of_isUpper toUpper_eq_of_not_isLower toNat_ofNat toLower_eq_of_not_isUpper
toUpper_toUpper_eq_toUpper 📖	—	—	—	—	toUpper_eq_of_not_isLower isLower_toUpper_eq_false

Char.beqCaseInsensitiveAsciiOnly

Definitions

Name	Category	Theorems
isSetoid 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eqv 📖	mathematical	—	Char.beqCaseInsensitiveAsciiOnly	—	—

---

← Back to Index