lemma
proved
term proof
acceptable_mono
No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
182lemma acceptable_mono {L : List SpeciesEntry}
183 {z₁ z₂ χ₁ χ₂ : ℝ}
184 (hz : z₁ ≤ z₂) (hχ : χ₁ ≤ χ₂) :
185 acceptable L z₁ χ₁ → acceptable L z₂ χ₂ := by
proof body
Term-mode proof.
186 intro h
187 rcases h with ⟨hzs, hchi⟩
188 refine And.intro ?hzs' ?hchi'
189 · intro e he; exact le_trans (hzs e he) hz
190 · exact le_trans hchi hχ
191
192/-- Monotonicity of all-species acceptability in the thresholds. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (14)
Lean names referenced from this declaration's body.
-
all
in IndisputableMonolith.Aesthetics.NarrativeGeodesic
decl_use
-
all
in IndisputableMonolith.Anthropology.KinshipGraphCohomology
decl_use
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
all
in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy
decl_use
-
le_trans
in IndisputableMonolith.Foundation.ArithmeticFromLogic
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
all
in IndisputableMonolith.Musicology.ModalPreferenceFromPhi
decl_use
-
acceptable
in IndisputableMonolith.PDG.Fits
decl_use
-
SpeciesEntry
in IndisputableMonolith.PDG.Fits
decl_use
-
L
in IndisputableMonolith.Recognition
decl_use
-
L
in IndisputableMonolith.Recognition.Cycle3
decl_use