Interval

📁 Source: Mathlib/Order/Filter/Interval.lean

Statistics

Metric	Count
Definitions `TendstoIxxClass`	1
Theorems `tendstoIxxClass`, `tendsto_Icc`, `Ico`, `Ioc`, `Ioo`, `uIcc`, `tendsto_Ixx`, `tendstoIxxClass_inf`, `tendstoIxxClass_of_subset`, `tendstoIxxClass_principal`, `tendsto_Icc_Icc_Icc`, `tendsto_Icc_atBot_atBot`, `tendsto_Icc_atTop_atTop`, `tendsto_Icc_pure_pure`, `tendsto_Icc_uIcc_uIcc`, `tendsto_Ico_Ici_Ici`, `tendsto_Ico_Iic_Iio`, `tendsto_Ico_Iio_Iio`, `tendsto_Ico_Ioi_Ioi`, `tendsto_Ico_atBot_atBot`, `tendsto_Ico_atTop_atTop`, `tendsto_Ico_pure_bot`, `tendsto_Ioc_Icc_Icc`, `tendsto_Ioc_Ici_Ioi`, `tendsto_Ioc_Iic_Iic`, `tendsto_Ioc_Iio_Iio`, `tendsto_Ioc_Ioi_Ioi`, `tendsto_Ioc_atBot_atBot`, `tendsto_Ioc_atTop_atTop`, `tendsto_Ioc_pure_bot`, `tendsto_Ioc_uIcc_uIcc`, `tendsto_Ioo_Ici_Ioi`, `tendsto_Ioo_Iic_Iio`, `tendsto_Ioo_Iio_Iio`, `tendsto_Ioo_Ioi_Ioi`, `tendsto_Ioo_atBot_atBot`, `tendsto_Ioo_atTop_atTop`, `tendsto_Ioo_pure_bot`, `tendsto_uIcc_of_Icc`	39
Total	40

Filter

Definitions

Name	Category	Theorems
`TendstoIxxClass` 📖	CompData	41 math math: `tendsto_Ioo_Iio_Iio`, `tendsto_Ico_pure_bot`, `tendsto_Ioc_Iio_Iio`, `tendstoIocClassNhds`, `tendstoIcoClassNhds`, `tendsto_Ioo_pure_bot`, `tendsto_Icc_atTop_atTop`, `tendsto_Ioc_pure_bot`, `OrdConnected.tendsto_Icc`, `HasBasis.tendstoIxxClass`, `tendsto_Ioc_atTop_atTop`, `tendsto_Ioc_Ici_Ioi`, `tendsto_Icc_Icc_Icc`, `tendsto_Ico_Ioi_Ioi`, `tendstoIxxClass_inf`, `tendsto_Ico_Iic_Iio`, `intervalIntegral.FTCFilter.toTendstoIxxClass`, `tendsto_Ioo_atTop_atTop`, `tendsto_Ioc_Icc_Icc`, `tendsto_Icc_atBot_atBot`, `tendstoIccClassNhds`, `tendsto_Ioo_atBot_atBot`, `tendsto_Ico_Ici_Ici`, `tendstoIxxClass_principal`, `tendsto_Ioo_Ici_Ioi`, `tendstoIccClassNhdsPi`, `tendsto_Ioo_Ioi_Ioi`, `tendsto_Ioc_uIcc_uIcc`, `tendsto_Icc_uIcc_uIcc`, `tendsto_Ioo_Iic_Iio`, `tendstoIxxClass_of_subset`, `tendsto_Ioc_Ioi_Ioi`, `tendsto_Icc_pure_pure`, `tendsto_Ioc_atBot_atBot`, `tendsto_Ico_Iio_Iio`, `tendsto_Ico_atTop_atTop`, `tendsto_uIcc_of_Icc`, `tendsto_Ico_atBot_atBot`, `tendstoIooClassNhds`, `tendstoIxxNhdsWithin`, `tendsto_Ioc_Iic_Iic`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tendstoIxxClass_inf` 📖	mathematical	—	`TendstoIxxClass` `Filter` `instInf`	—	`smallSets_inf` `prod_inf_prod` `Tendsto.inf` `TendstoIxxClass.tendsto_Ixx`
`tendstoIxxClass_of_subset` 📖	mathematical	`Set` `Set.instHasSubset`	`TendstoIxxClass`	—	`Tendsto.smallSets_mono` `TendstoIxxClass.tendsto_Ixx` `Eventually.of_forall`
`tendstoIxxClass_principal` 📖	mathematical	—	`TendstoIxxClass` `principal` `Set` `Set.instHasSubset`	—	`TendstoIxxClass.tendsto_Ixx` `prod_principal_principal` `smallSets_principal`
`tendsto_Icc_Icc_Icc` 📖	mathematical	—	`TendstoIxxClass` `Set.Icc` `principal`	—	`tendstoIxxClass_principal` `Set.Icc_subset_Icc`
`tendsto_Icc_atBot_atBot` 📖	mathematical	—	`TendstoIxxClass` `Set.Icc` `atBot`	—	`HasBasis.tendstoIxxClass` `hasBasis_iInf_principal_finite` `Set.OrdConnected.out` `Set.ordConnected_biInter` `Set.ordConnected_Iic`
`tendsto_Icc_atTop_atTop` 📖	mathematical	—	`TendstoIxxClass` `Set.Icc` `atTop`	—	`HasBasis.tendstoIxxClass` `hasBasis_iInf_principal_finite` `Set.OrdConnected.out` `Set.ordConnected_biInter` `Set.ordConnected_Ici`
`tendsto_Icc_pure_pure` 📖	mathematical	—	`TendstoIxxClass` `Set.Icc` `PartialOrder.toPreorder` `Filter` `instPure`	—	`principal_singleton` `tendstoIxxClass_principal` `Set.OrdConnected.out` `Set.ordConnected_singleton`
`tendsto_Icc_uIcc_uIcc` 📖	mathematical	—	`TendstoIxxClass` `Set.Icc` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `principal` `Set.uIcc`	—	`tendsto_Icc_Icc_Icc`
`tendsto_Ico_Ici_Ici` 📖	mathematical	—	`TendstoIxxClass` `Set.Ico` `principal` `Set.Ici`	—	`tendstoIxxClass_of_subset` `Set.Ico_subset_Icc_self` `OrdConnected.tendsto_Icc` `Set.ordConnected_Ici`
`tendsto_Ico_Iic_Iio` 📖	mathematical	—	`TendstoIxxClass` `Set.Ico` `principal` `Set.Iic` `Set.Iio`	—	`tendstoIxxClass_principal` `lt_of_lt_of_le`
`tendsto_Ico_Iio_Iio` 📖	mathematical	—	`TendstoIxxClass` `Set.Ico` `principal` `Set.Iio`	—	`tendstoIxxClass_of_subset` `Set.Ico_subset_Icc_self` `OrdConnected.tendsto_Icc` `Set.ordConnected_Iio`
`tendsto_Ico_Ioi_Ioi` 📖	mathematical	—	`TendstoIxxClass` `Set.Ico` `principal` `Set.Ioi`	—	`tendstoIxxClass_of_subset` `Set.Ico_subset_Icc_self` `OrdConnected.tendsto_Icc` `Set.ordConnected_Ioi`
`tendsto_Ico_atBot_atBot` 📖	mathematical	—	`TendstoIxxClass` `Set.Ico` `atBot`	—	`tendstoIxxClass_of_subset` `Set.Ico_subset_Icc_self` `tendsto_Icc_atBot_atBot`
`tendsto_Ico_atTop_atTop` 📖	mathematical	—	`TendstoIxxClass` `Set.Ico` `atTop`	—	`tendstoIxxClass_of_subset` `Set.Ico_subset_Icc_self` `tendsto_Icc_atTop_atTop`
`tendsto_Ico_pure_bot` 📖	mathematical	—	`TendstoIxxClass` `Set.Ico` `PartialOrder.toPreorder` `Filter` `instPure` `Bot.bot` `instBot`	—	`prod_pure` `smallSets_bot` `Set.Ico_eq_empty`
`tendsto_Ioc_Icc_Icc` 📖	mathematical	—	`TendstoIxxClass` `Set.Ioc` `principal` `Set.Icc`	—	`tendstoIxxClass_of_subset` `Set.Ioc_subset_Icc_self` `tendsto_Icc_Icc_Icc`
`tendsto_Ioc_Ici_Ioi` 📖	mathematical	—	`TendstoIxxClass` `Set.Ioc` `principal` `Set.Ici` `Set.Ioi`	—	`tendstoIxxClass_principal` `lt_of_le_of_lt`
`tendsto_Ioc_Iic_Iic` 📖	mathematical	—	`TendstoIxxClass` `Set.Ioc` `principal` `Set.Iic`	—	`tendstoIxxClass_of_subset` `Set.Ioc_subset_Icc_self` `OrdConnected.tendsto_Icc` `Set.ordConnected_Iic`
`tendsto_Ioc_Iio_Iio` 📖	mathematical	—	`TendstoIxxClass` `Set.Ioc` `principal` `Set.Iio`	—	`tendstoIxxClass_of_subset` `Set.Ioc_subset_Icc_self` `OrdConnected.tendsto_Icc` `Set.ordConnected_Iio`
`tendsto_Ioc_Ioi_Ioi` 📖	mathematical	—	`TendstoIxxClass` `Set.Ioc` `principal` `Set.Ioi`	—	`tendstoIxxClass_of_subset` `Set.Ioc_subset_Icc_self` `OrdConnected.tendsto_Icc` `Set.ordConnected_Ioi`
`tendsto_Ioc_atBot_atBot` 📖	mathematical	—	`TendstoIxxClass` `Set.Ioc` `atBot`	—	`tendstoIxxClass_of_subset` `Set.Ioc_subset_Icc_self` `tendsto_Icc_atBot_atBot`
`tendsto_Ioc_atTop_atTop` 📖	mathematical	—	`TendstoIxxClass` `Set.Ioc` `atTop`	—	`tendstoIxxClass_of_subset` `Set.Ioc_subset_Icc_self` `tendsto_Icc_atTop_atTop`
`tendsto_Ioc_pure_bot` 📖	mathematical	—	`TendstoIxxClass` `Set.Ioc` `PartialOrder.toPreorder` `Filter` `instPure` `Bot.bot` `instBot`	—	`prod_pure` `smallSets_bot` `Set.Ioc_eq_empty`
`tendsto_Ioc_uIcc_uIcc` 📖	mathematical	—	`TendstoIxxClass` `Set.Ioc` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `principal` `Set.uIcc`	—	`tendsto_Ioc_Icc_Icc`
`tendsto_Ioo_Ici_Ioi` 📖	mathematical	—	`TendstoIxxClass` `Set.Ioo` `principal` `Set.Ici` `Set.Ioi`	—	`tendstoIxxClass_of_subset` `Set.Ioo_subset_Ioc_self` `tendsto_Ioc_Ici_Ioi`
`tendsto_Ioo_Iic_Iio` 📖	mathematical	—	`TendstoIxxClass` `Set.Ioo` `principal` `Set.Iic` `Set.Iio`	—	`tendstoIxxClass_of_subset` `Set.Ioo_subset_Ico_self` `tendsto_Ico_Iic_Iio`
`tendsto_Ioo_Iio_Iio` 📖	mathematical	—	`TendstoIxxClass` `Set.Ioo` `principal` `Set.Iio`	—	`tendstoIxxClass_of_subset` `Set.Ioo_subset_Ioc_self` `tendsto_Ioc_Iio_Iio`
`tendsto_Ioo_Ioi_Ioi` 📖	mathematical	—	`TendstoIxxClass` `Set.Ioo` `principal` `Set.Ioi`	—	`tendstoIxxClass_of_subset` `Set.Ioo_subset_Ioc_self` `tendsto_Ioc_Ioi_Ioi`
`tendsto_Ioo_atBot_atBot` 📖	mathematical	—	`TendstoIxxClass` `Set.Ioo` `atBot`	—	`tendstoIxxClass_of_subset` `Set.Ioo_subset_Icc_self` `tendsto_Icc_atBot_atBot`
`tendsto_Ioo_atTop_atTop` 📖	mathematical	—	`TendstoIxxClass` `Set.Ioo` `atTop`	—	`tendstoIxxClass_of_subset` `Set.Ioo_subset_Icc_self` `tendsto_Icc_atTop_atTop`
`tendsto_Ioo_pure_bot` 📖	mathematical	—	`TendstoIxxClass` `Set.Ioo` `PartialOrder.toPreorder` `Filter` `instPure` `Bot.bot` `instBot`	—	`prod_pure` `smallSets_bot` `Set.Ioo_eq_empty`
`tendsto_uIcc_of_Icc` 📖	mathematical	—	`TendstoIxxClass` `Set.uIcc` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`mem_map` `mem_prod_self_iff` `Tendsto.Icc` `tendsto_fst` `tendsto_snd` `le_total` `Set.mem_preimage` `Set.uIcc_of_le` `Set.uIcc_of_ge`

Filter.HasBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tendstoIxxClass` 📖	mathematical	`Filter.HasBasis` `Set` `Set.instHasSubset`	`Filter.TendstoIxxClass`	—	`tendsto_iff` `prod_self` `smallSets`

Filter.OrdConnected

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tendsto_Icc` 📖	mathematical	—	`Filter.TendstoIxxClass` `Set.Icc` `Filter.principal`	—	`Filter.tendstoIxxClass_principal` `Set.OrdConnected.out`

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Ico` 📖	mathematical	`Filter.Tendsto`	`Set` `Set.Ico` `Filter.smallSets`	—	`comp` `Filter.TendstoIxxClass.tendsto_Ixx` `prodMk`
`Ioc` 📖	mathematical	`Filter.Tendsto`	`Set` `Set.Ioc` `Filter.smallSets`	—	`comp` `Filter.TendstoIxxClass.tendsto_Ixx` `prodMk`
`Ioo` 📖	mathematical	`Filter.Tendsto`	`Set` `Set.Ioo` `Filter.smallSets`	—	`comp` `Filter.TendstoIxxClass.tendsto_Ixx` `prodMk`
`uIcc` 📖	mathematical	`Filter.Tendsto`	`Set` `Set.uIcc` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Filter.smallSets`	—	`comp` `Filter.TendstoIxxClass.tendsto_Ixx` `Filter.tendsto_uIcc_of_Icc` `prodMk`

Filter.TendstoIxxClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tendsto_Ixx` 📖	mathematical	—	`Filter.Tendsto` `Set` `SProd.sprod` `Filter` `Filter.instSProd` `Filter.smallSets`	—	—

---

← Back to Index