Uniformly

📁 Source: PrimeNumberTheoremAnd/Mathlib/Analysis/Asymptotics/Uniformly.lean

Statistics

Metric	Count
Definitions	0
Theorems isBigO_of_isBigOUniformly, isBigO_rev_of_isBigOUniformly_rev, isLittleO_const_fst_atBot, isLittleO_const_fst_atTop, isLittleO_const_snd_atBot, isLittleO_const_snd_atTop, isTheta_of_isThetaUniformly, const_isBigOUniformlyOn_isCompact, const_isBigOUniformlyOn_isCompact_rev, const_isBigOWithUniformlyOn_isCompact, const_isBigOWithUniformlyOn_isCompact_rev, const_isThetaUniformlyOn_isCompact	12
Total	12

Asymptotics

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isBigO_of_isBigOUniformly 📖	—	—	—	—	—
isBigO_rev_of_isBigOUniformly_rev 📖	—	—	—	—	—
isLittleO_const_fst_atBot 📖	—	—	—	—	isLittleO_const_id_atBot2
isLittleO_const_fst_atTop 📖	—	—	—	—	isLittleO_const_id_atTop2
isLittleO_const_snd_atBot 📖	—	—	—	—	isLittleO_const_id_atBot2
isLittleO_const_snd_atTop 📖	—	—	—	—	isLittleO_const_id_atTop2
isTheta_of_isThetaUniformly 📖	—	—	—	—	isBigO_of_isBigOUniformly isBigO_rev_of_isBigOUniformly_rev

ContinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
const_isBigOUniformlyOn_isCompact 📖	—	—	—	—	const_isBigOWithUniformlyOn_isCompact
const_isBigOUniformlyOn_isCompact_rev 📖	—	—	—	—	const_isBigOWithUniformlyOn_isCompact_rev
const_isBigOWithUniformlyOn_isCompact 📖	—	—	—	—	—
const_isBigOWithUniformlyOn_isCompact_rev 📖	—	—	—	—	—
const_isThetaUniformlyOn_isCompact 📖	—	—	—	—	const_isBigOUniformlyOn_isCompact const_isBigOUniformlyOn_isCompact_rev

---

← Back to Index