`BookProof.ChapterBoseEinstein.boseEinstein_strictAntiOn` : StrictAntiOn boseEinstein (Set.Ioi 0)
ProvedBookProof.ChapterBoseEinstein.boseEinstein_strictAntiOntheoremstimepiece
Prove the following Lean 4 theorem from ChapterBoseEinstein.
BookProof.ChapterBoseEinstein.boseEinstein_strictAntiOn : StrictAntiOn boseEinstein (Set.Ioi 0)
Formalization note: Lean 4 identifier BookProof.ChapterBoseEinstein.boseEinstein_strictAntiOn.
Preamble
-- Generated from ChapterBoseEinstein.lean — theorem BookProof.ChapterBoseEinstein.boseEinstein_strictAntiOn
import Definitions.Def_ChapterCoherentTemperature
import Definitions.Def_ChapterCoherentOccupation
import Mathlib
import Definitions.Def_ChapterBoseEinstein
open BookProof.ChapterBoseEinstein
noncomputable section
open Filter Topology
open BookProof.ChapterCoherentTemperature BookProof.ChapterCoherentOccupation
variable {x : ℝ}Formal statement
theorem BookProof.ChapterBoseEinstein.boseEinstein_strictAntiOn : StrictAntiOn boseEinstein (Set.Ioi 0) := by sorry