def
definition
oscillatoryDynamicsCert
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.OscillatoryDynamicsDeep on GitHub at line 68.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
65 energy_pos : ∀ n : ℕ, 0 < energy_level n
66 energy_increasing : ∀ n : ℕ, energy_level n < energy_level (n + 1)
67
68noncomputable def oscillatoryDynamicsCert : OscillatoryDynamicsCert where
69 omega_pos := omega_pos
70 energy_pos := energy_pos
71 energy_increasing := energy_increasing
72
73theorem oscillatoryDynamicsCert_inhabited : Nonempty OscillatoryDynamicsCert :=
74 ⟨oscillatoryDynamicsCert⟩
75
76end
77end OscillatoryDynamicsDeep
78end Foundation
79end IndisputableMonolith