Floor

📁 Source: Mathlib/MeasureTheory/Function/Floor.lean

Statistics

Metric	Count
Definitions	0
Theorems measurable_ceil, measurable_floor, ceil, floor, fract, nat_ceil, nat_floor, image_fract, measurable_ceil, measurable_floor, measurable_fract	11
Total	11

Int

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measurable_ceil 📖	mathematical	—	Measurable instMeasurableSpace ceil	—	measurable_to_countable instCountableInt preimage_ceil_singleton measurableSet_Ioc instClosedIicTopology OrderTopology.to_orderClosedTopology
measurable_floor 📖	mathematical	—	Measurable instMeasurableSpace floor	—	measurable_to_countable instCountableInt preimage_floor_singleton measurableSet_Ico instClosedIciTopology OrderTopology.to_orderClosedTopology

Measurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ceil 📖	mathematical	Measurable	Int.instMeasurableSpace Int.ceil	—	comp Int.measurable_ceil
floor 📖	mathematical	Measurable	Int.instMeasurableSpace Int.floor	—	comp Int.measurable_floor
fract 📖	mathematical	Measurable	Int.fract	—	comp measurable_fract
nat_ceil 📖	mathematical	Measurable	Nat.instMeasurableSpace Nat.ceil SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	comp Nat.measurable_ceil
nat_floor 📖	mathematical	Measurable	Nat.instMeasurableSpace Nat.floor SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	comp Nat.measurable_floor

MeasurableSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
image_fract 📖	mathematical	MeasurableSet	Set.image Int.fract	—	Int.image_fract Set.image_congr sub_eq_add_neg Set.image_add_right' iUnion instCountableInt inter MeasurableAdd.measurable_add_const ContinuousAdd.measurableAdd IsTopologicalAddGroup.toContinuousAdd LinearOrderedAddCommGroup.toIsTopologicalAddGroup IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing measurableSet_Ico BorelSpace.opensMeasurable instClosedIciTopology OrderTopology.to_orderClosedTopology

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measurable_ceil 📖	mathematical	—	Measurable instMeasurableSpace ceil SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	measurable_to_countable instCountableNat eq_or_ne preimage_ceil_zero instClosedIicTopology OrderTopology.to_orderClosedTopology preimage_ceil_of_ne_zero
measurable_floor 📖	mathematical	—	Measurable instMeasurableSpace floor SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	measurable_to_countable instCountableNat eq_or_ne preimage_floor_zero instClosedIciTopology OrderTopology.to_orderClosedTopology preimage_floor_of_ne_zero

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measurable_fract 📖	mathematical	—	Measurable Int.fract	—	Int.preimage_fract MeasurableSet.iUnion instCountableInt Measurable.sub_const ContinuousSub.measurableSub IsTopologicalAddGroup.to_continuousSub LinearOrderedAddCommGroup.toIsTopologicalAddGroup IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing measurable_id MeasurableSet.inter measurableSet_Ico BorelSpace.opensMeasurable instClosedIciTopology OrderTopology.to_orderClosedTopology

---

← Back to Index