Floor

📁 Source: Mathlib/Topology/Algebra/Order/Floor.lean

Statistics

Metric	Count
Definitions	0
Theorems comp_fract, comp_fract', comp_fract'', tendsto_mul_pow_div_factorial_sub_atTop, tendsto_pow_div_factorial_atTop, continuousAt_fract, continuousOn_ceil, continuousOn_floor, continuousOn_fract, tendsto_ceil_atBot, tendsto_ceil_atTop, tendsto_ceil_left, tendsto_ceil_left', tendsto_ceil_left_pure, tendsto_ceil_left_pure_ceil, tendsto_ceil_right, tendsto_ceil_right', tendsto_ceil_right_pure_add_one, tendsto_ceil_right_pure_floor_add_one, tendsto_floor_atBot, tendsto_floor_atTop, tendsto_floor_left, tendsto_floor_left', tendsto_floor_left_pure_ceil_sub_one, tendsto_floor_left_pure_sub_one, tendsto_floor_right, tendsto_floor_right', tendsto_floor_right_pure, tendsto_floor_right_pure_floor, tendsto_fract_left, tendsto_fract_left', tendsto_fract_right, tendsto_fract_right'	33
Total	33

ContinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_fract 📖	mathematical	ContinuousOn instTopologicalSpaceProd SProd.sprod Set Set.instSProd Set.univ Set.Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Continuous	Int.fract	—	Continuous.comp comp_fract' Continuous.prodMk continuous_id
comp_fract' 📖	mathematical	ContinuousOn instTopologicalSpaceProd SProd.sprod Set Set.instSProd Set.univ Set.Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	Continuous Int.fract	—	continuous_iff_continuousAt em ContinuousAt.eq_1 nhds_prod_eq nhdsLT_sup_nhdsGE Filter.prod_sup Filter.tendsto_sup Filter.Tendsto.mono_right Filter.Tendsto.comp Filter.Tendsto.mono_left ContinuousWithinAt.tendsto zero_le_one IsStrictOrderedRing.toZeroLEOneClass le_rfl nhdsWithin_prod_eq nhdsWithin_univ nhdsWithin_Ico_eq_nhdsLT instClosedIicTopology OrderTopology.to_orderClosedTopology one_pos NeZero.charZero_one IsStrictOrderedRing.toCharZero Filter.prod_mono nhdsWithin_mono Set.Ico_subset_Icc_self Filter.Tendsto.prodMap Filter.tendsto_id tendsto_fract_left LinearOrderedAddCommGroup.toIsTopologicalAddGroup IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing le_of_eq Int.fract_intCast nhdsWithin_Icc_eq_nhdsGE instClosedIciTopology tendsto_fract_right ContinuousAt.comp continuousAt prod_mem_nhds Filter.univ_mem Icc_mem_nhds Int.fract_pos Int.fract_lt_one ContinuousAt.prodMap continuousAt_id continuousAt_fract
comp_fract'' 📖	mathematical	ContinuousOn Set.Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	Continuous Int.fract	—	comp_fract comp continuousOn_snd Set.mem_prod continuous_id

FloorSemiring

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tendsto_mul_pow_div_factorial_sub_atTop 📖	mathematical	—	Filter.Tendsto DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Nat.factorial Filter.atTop Nat.instPreorder nhds MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	tendsto_order Filter.mp_mem eventually_mul_pow_lt_factorial_sub Filter.univ_mem' lt_div_iff₀' PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Nat.cast_pos IsStrictOrderedRing.toIsOrderedRing instNontrivialOfCharZero IsStrictOrderedRing.toCharZero Nat.factorial_pos div_lt_iff_of_neg div_eq_mul_inv mul_right_comm div_lt_iff₀' div_lt_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono
tendsto_pow_div_factorial_atTop 📖	mathematical	—	Filter.Tendsto DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Nat.factorial Filter.atTop Nat.instPreorder nhds MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	—	one_mul tendsto_mul_pow_div_factorial_sub_atTop

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousAt_fract 📖	mathematical	—	ContinuousAt Int.fract	—	ContinuousOn.continuousAt continuousOn_fract Ico_mem_nhds LE.le.lt_of_ne Int.floor_le Int.lt_floor_add_one
continuousOn_ceil 📖	mathematical	—	ContinuousOn AddGroupWithOne.toIntCast Ring.toAddGroupWithOne Int.ceil Set.Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	—	continuousOn_congr Int.ceil_eq_on_Ioc' continuousOn_const
continuousOn_floor 📖	mathematical	—	ContinuousOn AddGroupWithOne.toIntCast Ring.toAddGroupWithOne Int.floor Set.Ico PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	—	continuousOn_congr Int.floor_eq_on_Ico' continuousOn_const
continuousOn_fract 📖	mathematical	—	ContinuousOn Int.fract Set.Ico PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddGroupWithOne.toIntCast Ring.toAddGroupWithOne Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	—	ContinuousOn.sub IsTopologicalAddGroup.to_continuousSub continuousOn_id continuousOn_floor
tendsto_ceil_atBot 📖	mathematical	—	Filter.Tendsto Int.ceil Filter.atBot PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLatticeInt	—	Monotone.tendsto_atBot_atBot Int.ceil_mono Int.ceil_intCast LT.lt.le sub_one_lt Int.instZeroLEOneClass IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd Int.instAddLeftMono
tendsto_ceil_atTop 📖	mathematical	—	Filter.Tendsto Int.ceil Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLatticeInt	—	Monotone.tendsto_atTop_atTop Int.ceil_mono Eq.ge Int.ceil_intCast
tendsto_ceil_left 📖	mathematical	—	Filter.Tendsto AddGroupWithOne.toIntCast Ring.toAddGroupWithOne Int.ceil nhdsWithin Set.Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Filter.Tendsto.mono_right Filter.Tendsto.comp Filter.tendsto_pure_pure tendsto_ceil_left_pure pure_le_nhdsWithin le_rfl
tendsto_ceil_left' 📖	mathematical	—	Filter.Tendsto AddGroupWithOne.toIntCast Ring.toAddGroupWithOne Int.ceil nhdsWithin Set.Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder nhds	—	Filter.Tendsto.mono_right tendsto_ceil_left inf_le_left
tendsto_ceil_left_pure 📖	mathematical	—	Filter.Tendsto Int.ceil nhdsWithin AddGroupWithOne.toIntCast Ring.toAddGroupWithOne Set.Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Filter Filter.instPure	—	Int.ceil_intCast tendsto_ceil_left_pure_ceil
tendsto_ceil_left_pure_ceil 📖	mathematical	—	Filter.Tendsto Int.ceil nhdsWithin Set.Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Filter Filter.instPure	—	Filter.tendsto_pure Filter.mem_of_superset Ioc_mem_nhdsLE instClosedIicTopology sub_lt_iff_lt_add IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing Int.ceil_lt_add_one Int.ceil_eq_on_Ioc LE.le.trans Int.le_ceil
tendsto_ceil_right 📖	mathematical	—	Filter.Tendsto AddGroupWithOne.toIntCast Ring.toAddGroupWithOne Int.ceil nhdsWithin Set.Ioi PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Set.Ici	—	Filter.Tendsto.mono_right Filter.Tendsto.comp Filter.tendsto_pure_pure tendsto_ceil_right_pure_add_one Int.cast_one Int.cast_add pure_le_nhdsWithin le_rfl
tendsto_ceil_right' 📖	mathematical	—	Filter.Tendsto AddGroupWithOne.toIntCast Ring.toAddGroupWithOne Int.ceil nhdsWithin Set.Ioi PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder nhds Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	—	Filter.Tendsto.mono_right tendsto_ceil_right inf_le_left
tendsto_ceil_right_pure_add_one 📖	mathematical	—	Filter.Tendsto Int.ceil nhdsWithin AddGroupWithOne.toIntCast Ring.toAddGroupWithOne Set.Ioi PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Filter Filter.instPure	—	Int.floor_intCast tendsto_ceil_right_pure_floor_add_one
tendsto_ceil_right_pure_floor_add_one 📖	mathematical	—	Filter.Tendsto Int.ceil nhdsWithin Set.Ioi PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Filter Filter.instPure Int.floor	—	Int.cast_add Int.cast_one add_sub_cancel_right Int.floor_le Filter.tendsto_pure Filter.mem_of_superset Ioc_mem_nhdsGT instClosedIciTopology Int.lt_succ_floor Int.ceil_eq_on_Ioc LE.le.trans_lt
tendsto_floor_atBot 📖	mathematical	—	Filter.Tendsto Int.floor Filter.atBot PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLatticeInt	—	Monotone.tendsto_atBot_atBot Int.floor_mono Eq.le Int.floor_intCast
tendsto_floor_atTop 📖	mathematical	—	Filter.Tendsto Int.floor Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLatticeInt	—	Monotone.tendsto_atTop_atTop Int.floor_mono Int.floor_intCast LT.lt.le lt_add_one Int.instZeroLEOneClass IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd Int.instAddLeftMono
tendsto_floor_left 📖	mathematical	—	Filter.Tendsto AddGroupWithOne.toIntCast Ring.toAddGroupWithOne Int.floor nhdsWithin Set.Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Set.Iic	—	Filter.Tendsto.mono_right Filter.Tendsto.comp Filter.tendsto_pure_pure tendsto_floor_left_pure_sub_one Int.cast_one Int.cast_sub pure_le_nhdsWithin le_rfl
tendsto_floor_left' 📖	mathematical	—	Filter.Tendsto AddGroupWithOne.toIntCast Ring.toAddGroupWithOne Int.floor nhdsWithin Set.Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder nhds SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	—	Filter.Tendsto.mono_right tendsto_floor_left inf_le_left
tendsto_floor_left_pure_ceil_sub_one 📖	mathematical	—	Filter.Tendsto Int.floor nhdsWithin Set.Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Filter Filter.instPure Int.ceil	—	Int.cast_sub Int.cast_one sub_lt_iff_lt_add IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing Int.ceil_lt_add_one sub_add_cancel Int.le_ceil Filter.tendsto_pure Filter.mem_of_superset Ico_mem_nhdsLT instClosedIicTopology Int.floor_eq_on_Ico LT.lt.trans_le
tendsto_floor_left_pure_sub_one 📖	mathematical	—	Filter.Tendsto Int.floor nhdsWithin AddGroupWithOne.toIntCast Ring.toAddGroupWithOne Set.Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Filter Filter.instPure	—	Int.ceil_intCast tendsto_floor_left_pure_ceil_sub_one
tendsto_floor_right 📖	mathematical	—	Filter.Tendsto AddGroupWithOne.toIntCast Ring.toAddGroupWithOne Int.floor nhdsWithin Set.Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Filter.Tendsto.mono_right Filter.Tendsto.comp Filter.tendsto_pure_pure tendsto_floor_right_pure pure_le_nhdsWithin le_rfl
tendsto_floor_right' 📖	mathematical	—	Filter.Tendsto AddGroupWithOne.toIntCast Ring.toAddGroupWithOne Int.floor nhdsWithin Set.Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder nhds	—	Filter.Tendsto.mono_right tendsto_floor_right inf_le_left
tendsto_floor_right_pure 📖	mathematical	—	Filter.Tendsto Int.floor nhdsWithin AddGroupWithOne.toIntCast Ring.toAddGroupWithOne Set.Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Filter Filter.instPure	—	Int.floor_intCast tendsto_floor_right_pure_floor
tendsto_floor_right_pure_floor 📖	mathematical	—	Filter.Tendsto Int.floor nhdsWithin Set.Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Filter Filter.instPure	—	Filter.tendsto_pure Filter.mem_of_superset Ico_mem_nhdsGE instClosedIciTopology Int.lt_floor_add_one Int.floor_eq_on_Ico LE.le.trans Int.floor_le
tendsto_fract_left 📖	mathematical	—	Filter.Tendsto Int.fract nhdsWithin AddGroupWithOne.toIntCast Ring.toAddGroupWithOne Set.Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	—	tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within tendsto_fract_left' Filter.Eventually.of_forall Int.fract_lt_one
tendsto_fract_left' 📖	mathematical	—	Filter.Tendsto Int.fract nhdsWithin AddGroupWithOne.toIntCast Ring.toAddGroupWithOne Set.Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder nhds AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	—	sub_sub_cancel Filter.Tendsto.sub IsTopologicalAddGroup.to_continuousSub Filter.Tendsto.mono_left Filter.tendsto_id nhdsWithin_le_nhds tendsto_floor_left'
tendsto_fract_right 📖	mathematical	—	Filter.Tendsto Int.fract nhdsWithin AddGroupWithOne.toIntCast Ring.toAddGroupWithOne Set.Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within tendsto_fract_right' Filter.Eventually.of_forall Int.fract_nonneg
tendsto_fract_right' 📖	mathematical	—	Filter.Tendsto Int.fract nhdsWithin AddGroupWithOne.toIntCast Ring.toAddGroupWithOne Set.Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder nhds MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	Filter.Tendsto.sub IsTopologicalAddGroup.to_continuousSub tendsto_nhdsWithin_of_tendsto_nhds Filter.tendsto_id tendsto_floor_right' sub_self

---

← Back to Index