def
definition
cert
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Sociology.SocialStratificationFromConfigDim on GitHub at line 75.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
72 cost_nonneg : ∀ a e : ℝ, 0 < a → 0 < e → 0 ≤ mobilityTransitionCost a e
73 mobility_cost_pos : 0 < oneStepMobilityCost
74
75noncomputable def cert : SocialStratificationCert where
76 stratum_count := socialStratumCount_eq
77 cost_at_stratum := mobilityTransitionCost_at_stratum
78 cost_nonneg := mobilityTransitionCost_nonneg
79 mobility_cost_pos := oneStepMobilityCost_pos
80
81theorem cert_inhabited : Nonempty SocialStratificationCert := ⟨cert⟩
82
83end
84end SocialStratificationFromConfigDim
85end Sociology
86end IndisputableMonolith