recognition / Compat / Compat.Constants / l0_pos

lemma

`l0_pos`

proved

show as: view math explainer →

module: IndisputableMonolith.Compat.Constants
domain: Compat
line: 30 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Compat.Constants on GitHub at line 30.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

depends on

formal source

  27
  28/-- Fundamental length ℓ₀ (placeholder) -/
  29def l0 : ℝ := 1
  30lemma l0_pos : 0 < l0 := by
  31  simpa [l0] using (zero_lt_one : 0 < (1 : ℝ))
  32
  33end
  34
  35end Constants
  36
  37namespace RSBridge
  38namespace Fermion
  39
  40def rung : ℕ := 1
  41
  42end Fermion
  43end RSBridge

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.