Mathlib Map

Theorems · Theorem · logic and foundations

add_lt_ack

∀ (m n : ℕ), m + n < ack m n
Defined in
Mathlib.Computability.Ackermann
Cited by
4 results in Mathlib
Foundations
Depth 60 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

add_add_one_le_ack · cited by 1add_add_one_le_acklt_ack_right · cited by 1lt_ack_rightexists_lt_ack_of_nat_primrec · cited by 1exists_lt_ack_of_nat_prim…lt_ack_left · cited by 0lt_ack_leftack · cited by 41ackadd_lt_ackCITED BYCITES

Cites1

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • ackstatement · cited by 41

Cited by4

Results whose statement or proof uses this declaration.