`BookProof.EnergyBandDecomposition.mem_band_iff_floor` (hε : 0 < ε) (E : X → ℝ) (k : ℤ) (x : X) : x ∈ band E ε k ↔ k = ⌊E x / ε⌋

Initializing...

`BookProof.EnergyBandDecomposition.mem_band_iff_floor` (hε : 0 < ε) (E : X → ℝ) (k : ℤ) (x : X) : x ∈ band E ε k ↔ k = ⌊E x / ε⌋ · Prove2Me