Mathlib Map

Theorems · Definition · order theory

ENat.floor

ENNReal → ℕ∞

⌊r⌋ₑ is the greatest extended natural n such that n ≤ r.

Defined in
Mathlib.Algebra.Order.Floor.Extended
Cited by
38 results in Mathlib
Foundations
Depth 113 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

ENat.floor_natCast · cited by 3ENat.floor_natCastENat.floor_sub_toENNReal · cited by 3ENat.floor_sub_toENNRealENat.le_floor · cited by 3ENat.le_floorENat.floor_add_natCast · cited by 2ENat.floor_add_natCastENat.floor_add_toENNReal · cited by 2ENat.floor_add_toENNRealENat.floor_le_self · cited by 2ENat.floor_le_selfENat.floor_lt · cited by 1ENat.floor_ltENat.floor_mono · cited by 1ENat.floor_monoENat.floor_toENNReal_add · cited by 1ENat.floor_toENNReal_addENat.floor_zero · cited by 1ENat.floor_zeroENat.preimage_toENNReal_Ioi · cited by 1ENat.preimage_toENNReal_I…ENat.lt_floor · cited by 0ENat.lt_floorENat.toENNReal_iSup · cited by 0ENat.toENNReal_iSupENat.floor_add_ofNat · cited by 0ENat.floor_add_ofNatENat.floor_add_one · cited by 0ENat.floor_add_oneENNReal · cited by 9879ENNRealTop.top · cited by 9680Top.topENat · cited by 4985ENatNNReal · cited by 4310NNRealNat.floor · cited by 215Nat.floorENat.floorCITED BYCITES

Cites5

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • ENNRealstatement and proof · cited by 9,879
  • Top.topproof · cited by 9,680
  • ENatstatement and proof · cited by 4,985
  • NNRealproof · cited by 4,310
  • Nat.floorproof · cited by 215

Cited by38

Results whose statement or proof uses this declaration.