Log

Statistics

Metric	Count
Definitions `clog`, `go`, `go`	3
Theorems `add_pred_div_lt`, `go_spec`, `clog_anti_left`, `clog_antitone_left`, `clog_eq_clog_succ_iff`, `clog_eq_one`, `clog_le_iff_le_pow`, `clog_le_of_le_pow`, `clog_lt_clog_succ_iff`, `clog_mono`, `clog_mono_right`, `clog_monotone`, `clog_of_left_le_one`, `clog_of_one_lt`, `clog_of_right_le_one`, `clog_of_two_le`, `clog_one_left`, `clog_one_right`, `clog_pos`, `clog_pow`, `clog_pow_left`, `clog_zero_left`, `clog_zero_right`, `le_log_iff_pow_le`, `le_log_of_pow_le`, `le_pow_clog`, `le_pow_iff_clog_le`, `go_spec`, `log2_eq_log_two`, `log_anti_left`, `log_antitone_left`, `log_div_base`, `log_div_base_pow`, `log_div_mul_self`, `log_eq_iff`, `log_eq_log_succ_iff`, `log_eq_of_pow_le_of_lt_pow`, `log_eq_one_iff`, `log_eq_one_iff'`, `log_eq_zero_iff`, `log_le_clog`, `log_le_self`, `log_lt_iff_lt_pow`, `log_lt_log_succ_iff`, `log_lt_of_lt_pow`, `log_lt_of_lt_pow'`, `log_lt_self`, `log_mono`, `log_mono_right`, `log_monotone`, `log_mul_base`, `log_of_left_le_one`, `log_of_lt`, `log_of_one_lt_of_le`, `log_one_left`, `log_one_right`, `log_pos`, `log_pos_iff`, `log_pow`, `log_pow_left`, `log_two_bit`, `log_zero_left`, `log_zero_right`, `lt_clog_iff_pow_lt`, `lt_pow_iff_log_lt`, `lt_pow_of_log_lt`, `lt_pow_succ_log_self`, `pow_le_iff_le_log`, `pow_le_of_le_log`, `pow_log_le_add_one`, `pow_log_le_self`, `pow_lt_iff_lt_clog`, `pow_lt_of_lt_clog`, `pow_pred_clog_lt_self`	74
Total	77

Nat

Definitions

Name	Category	Theorems
`clog` 📖	CompOp	33 math math: `le_pow_iff_clog_le`, `clog_of_right_le_one`, `clog_one_left`, `clog_antitone_left`, `lt_clog_iff_pow_lt`, `clog_le_iff_le_pow`, `clog_monotone`, `Real.natCeil_logb_natCast`, `clog_pow_left`, `clog_of_two_le`, `le_pow_clog`, `clog_eq_clog_succ_iff`, `pow_pred_clog_lt_self`, `Int.clog_of_one_le_right`, `clog_pow`, `clog_lt_clog_succ_iff`, `log_le_clog`, `clog_zero_left`, `Int.clog_natCast`, `clog_of_left_le_one`, `clog_one_right`, `clog_zero_right`, `clog_mono`, `clog_eq_one`, `Int.log_of_right_le_one`, `Mathlib.Meta.NormNum.nat_clog_helper`, `Int.clog_ofNat`, `pow_lt_iff_lt_clog`, `clog_pos`, `clog_mono_right`, `clog_of_one_lt`, `clog_le_of_le_pow`, `clog_anti_left`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_pred_div_lt` 📖	—	—	—	—	—
`clog_anti_left` 📖	mathematical	—	`clog`	—	`clog_le_iff_le_pow` `lt_of_lt_of_le` `le_pow_clog`
`clog_antitone_left` 📖	mathematical	—	`AntitoneOn` `instPreorder` `clog` `Set.Ioi`	—	`clog_anti_left` `Set.mem_Iio`
`clog_eq_clog_succ_iff` 📖	mathematical	—	`clog`	—	`clog_lt_clog_succ_iff` `not_lt` `clog_monotone`
`clog_eq_one` 📖	mathematical	—	`clog`	—	`clog_of_two_le` `LE.le.trans` `clog_of_right_le_one`
`clog_le_iff_le_pow` 📖	mathematical	—	`clog`	—	`clog.fun_cases_unfolding` `clog.go_spec`
`clog_le_of_le_pow` 📖	mathematical	—	`clog`	—	`clog_le_iff_le_pow`
`clog_lt_clog_succ_iff` 📖	mathematical	—	`clog`	—	`le_antisymm` `lt_clog_iff_pow_lt` `le_pow_clog`
`clog_mono` 📖	mathematical	—	`clog`	—	`LE.le.trans` `clog_anti_left` `clog_mono_right`
`clog_mono_right` 📖	mathematical	—	`clog`	—	`le_or_gt` `clog_of_left_le_one` `clog_le_iff_le_pow` `LE.le.trans` `le_pow_clog`
`clog_monotone` 📖	mathematical	—	`Monotone` `instPreorder` `clog`	—	`clog_mono_right`
`clog_of_left_le_one` 📖	mathematical	—	`clog`	—	—
`clog_of_one_lt` 📖	mathematical	—	`clog`	—	`eq_of_forall_ge_iff` `clog_pos`
`clog_of_right_le_one` 📖	mathematical	—	`clog`	—	—
`clog_of_two_le` 📖	mathematical	—	`clog`	—	`clog_of_one_lt`
`clog_one_left` 📖	mathematical	—	`clog`	—	`clog_of_left_le_one` `le_rfl`
`clog_one_right` 📖	mathematical	—	`clog`	—	`clog_of_right_le_one` `le_rfl`
`clog_pos` 📖	mathematical	—	`clog`	—	`clog.eq_1`
`clog_pow` 📖	mathematical	—	`clog`	—	`eq_of_forall_ge_iff` `clog_le_iff_le_pow`
`clog_pow_left` 📖	mathematical	—	`clog`	—	`clog_one_left` `eq_of_forall_lt_iff` `lt_clog_iff_pow_lt`
`clog_zero_left` 📖	mathematical	—	`clog`	—	`clog_of_left_le_one`
`clog_zero_right` 📖	mathematical	—	`clog`	—	`clog_of_right_le_one`
`le_log_iff_pow_le` 📖	mathematical	—	`log`	—	`le_iff_le_iff_lt_iff_lt` `log_lt_iff_lt_pow`
`le_log_of_pow_le` 📖	mathematical	—	`log`	—	`ne_or_eq` `le_log_iff_pow_le` `LE.le.not_gt` `LT.lt.trans`
`le_pow_clog` 📖	mathematical	—	`clog`	—	`clog_le_iff_le_pow` `le_rfl`
`le_pow_iff_clog_le` 📖	mathematical	—	`clog`	—	`clog_le_iff_le_pow`
`log2_eq_log_two` 📖	mathematical	—	`log`	—	`eq_or_ne` `log_zero_right` `eq_of_forall_le_iff` `le_log_iff_pow_le`
`log_anti_left` 📖	mathematical	—	`log`	—	`eq_or_ne` `log_zero_right` `le_refl` `le_log_of_pow_le` `pow_log_le_self`
`log_antitone_left` 📖	mathematical	—	`AntitoneOn` `instPreorder` `log` `Set.Ioi`	—	`log_anti_left` `Set.mem_Iio`
`log_div_base` 📖	mathematical	—	`log`	—	`le_or_gt` `log_of_left_le_one` `lt_or_ge` `log_of_lt` `log_zero_right` `log_of_one_lt_of_le`
`log_div_base_pow` 📖	mathematical	—	`log`	—	`log_div_base`
`log_div_mul_self` 📖	mathematical	—	`log`	—	`le_or_gt` `log_of_left_le_one` `lt_or_ge` `log_zero_right` `log_of_lt` `log_mul_base` `LT.lt.ne'` `log_div_base` `log_pos`
`log_eq_iff` 📖	mathematical	—	`log`	—	`em` `le_antisymm_iff` `le_log_iff_pow_le` `log_lt_iff_lt_pow` `not_lt` `not_and_or` `log_zero_left` `log_one_left` `log_zero_right`
`log_eq_log_succ_iff` 📖	mathematical	—	`log`	—	`log_lt_log_succ_iff` `not_lt` `log_monotone`
`log_eq_of_pow_le_of_lt_pow` 📖	mathematical	—	`log`	—	`eq_or_ne` `log_of_lt` `log_eq_iff`
`log_eq_one_iff` 📖	mathematical	—	`log`	—	`log_eq_one_iff'` `LE.le.trans_lt`
`log_eq_one_iff'` 📖	mathematical	—	`log`	—	`log_eq_iff`
`log_eq_zero_iff` 📖	mathematical	—	`log`	—	`eq_or_ne` `log_lt_iff_lt_pow` `log_of_left_le_one`
`log_le_clog` 📖	mathematical	—	`log` `clog`	—	`le_or_gt` `log_of_left_le_one` `log_zero_right` `LE.le.trans` `pow_log_le_self` `le_pow_clog`
`log_le_self` 📖	mathematical	—	`log`	—	`log_zero_right` `LT.lt.le` `log_lt_self`
`log_lt_iff_lt_pow` 📖	mathematical	—	`log`	—	`log.go_spec` `log.eq_1`
`log_lt_log_succ_iff` 📖	mathematical	—	`log`	—	`le_antisymm` `pow_log_le_self` `lt_pow_of_log_lt` `log_lt_of_lt_pow`
`log_lt_of_lt_pow` 📖	mathematical	—	`log`	—	`lt_imp_lt_of_le_imp_le` `pow_le_of_le_log`
`log_lt_of_lt_pow'` 📖	mathematical	—	`log`	—	`eq_or_ne` `log_lt_of_lt_pow`
`log_lt_self` 📖	mathematical	—	`log`	—	`le_or_gt` `log_of_left_le_one` `log_lt_of_lt_pow`
`log_mono` 📖	mathematical	—	`log`	—	`LE.le.trans` `log_anti_left` `log_mono_right`
`log_mono_right` 📖	mathematical	—	`log`	—	`log_monotone`
`log_monotone` 📖	mathematical	—	`Monotone` `instPreorder` `log`	—	`monotone_nat_of_le_succ` `le_or_gt` `log_of_left_le_one` `le_log_of_pow_le` `pow_log_le_add_one`
`log_mul_base` 📖	mathematical	—	`log`	—	`log_eq_of_pow_le_of_lt_pow` `pow_log_le_self` `LT.lt.trans` `lt_pow_succ_log_self`
`log_of_left_le_one` 📖	mathematical	—	`log`	—	`log.eq_1`
`log_of_lt` 📖	mathematical	—	`log`	—	`log.fun_cases_unfolding` `log.go.fun_cases_unfolding`
`log_of_one_lt_of_le` 📖	mathematical	—	`log`	—	`eq_of_forall_gt_iff` `log_lt_iff_lt_pow`
`log_one_left` 📖	mathematical	—	`log`	—	`log_of_left_le_one` `le_rfl`
`log_one_right` 📖	mathematical	—	`log`	—	`log_eq_zero_iff` `lt_or_ge`
`log_pos` 📖	mathematical	—	`log`	—	`log_pos_iff`
`log_pos_iff` 📖	mathematical	—	`log`	—	`log_eq_zero_iff` `not_lt` `not_le`
`log_pow` 📖	mathematical	—	`log`	—	`log_eq_of_pow_le_of_lt_pow` `le_rfl`
`log_pow_left` 📖	mathematical	—	`log`	—	`eq_or_ne` `log_zero_right` `log_one_left` `eq_of_forall_le_iff` `le_log_iff_pow_le` `log_of_left_le_one`
`log_two_bit` 📖	mathematical	—	`log` `bit`	—	`log_div_mul_self` `bit_div_two` `log_mul_base`
`log_zero_left` 📖	mathematical	—	`log`	—	`log_of_left_le_one`
`log_zero_right` 📖	mathematical	—	`log`	—	`log_eq_zero_iff` `le_total`
`lt_clog_iff_pow_lt` 📖	mathematical	—	`clog`	—	`lt_iff_lt_of_le_iff_le` `clog_le_iff_le_pow`
`lt_pow_iff_log_lt` 📖	mathematical	—	`log`	—	`log_lt_iff_lt_pow`
`lt_pow_of_log_lt` 📖	—	`log`	—	—	`lt_imp_lt_of_le_imp_le` `le_log_of_pow_le`
`lt_pow_succ_log_self` 📖	mathematical	—	`log`	—	`lt_pow_of_log_lt`
`pow_le_iff_le_log` 📖	mathematical	—	`log`	—	`le_log_iff_pow_le`
`pow_le_of_le_log` 📖	—	`log`	—	—	`le_or_gt` `log_of_left_le_one` `le_log_iff_pow_le`
`pow_log_le_add_one` 📖	mathematical	—	`log`	—	`log_zero_right` `le_refl` `LE.le.trans` `pow_log_le_self`
`pow_log_le_self` 📖	mathematical	—	`log`	—	`pow_le_of_le_log` `le_rfl`
`pow_lt_iff_lt_clog` 📖	mathematical	—	`clog`	—	`lt_clog_iff_pow_lt`
`pow_lt_of_lt_clog` 📖	—	`clog`	—	—	`lt_imp_lt_of_le_imp_le` `clog_le_of_le_pow`
`pow_pred_clog_lt_self` 📖	mathematical	—	`clog`	—	`lt_clog_iff_pow_lt` `LT.lt.ne'` `clog_pos`

Nat.clog

Definitions

Name	Category	Theorems
`go` 📖	CompOp	1 math math: `go_spec`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`go_spec` 📖	mathematical	—	`go`	—	—

Nat.log

Definitions

Name	Category	Theorems
`go` 📖	CompOp	1 math math: `go_spec`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`go_spec` 📖	mathematical	—	`go`	—	—

---

← Back to Index