| Name | Category | Theorems |
|---|
uIcc π | CompOp | 143 mathmath: Complex.verticalSegment_eq, Fin.image_castSucc_uIcc, Complex.norm_circleTransformBoundingFunction_le, Fin.preimage_addNat_uIcc_addNat, uIcc_injective_left, intervalIntegrable_iff', Antitone.mapsTo_uIcc, OrdConnected.uIcc_subset, image_single_uIcc_right, image_const_mul_uIcc, Icc_min_max, Filter.Tendsto.uIcc, ordConnected_iff_uIcc_subset_left, Path.range_subpathAux, uIcc_subset_uIcc_iff_mem, NNReal.segment_eq_uIcc, finite_uIcc, nhdsWithin_uIcc_isMeasurablyGenerated, neg_uIcc, segment_eq_uIcc, uIcc_of_lt, image_mulSingle_uIcc_left, uIcc_of_not_ge, mem_uIcc_of_le, AbsolutelyContinuousOnInterval.boundedVariationOn, Nonneg.segment_eq_uIcc, closure_uIoo, uIcc_comm, preimage_add_const_uIcc, strictConvex_uIcc, Icc_subset_uIcc, uIcc_prod_uIcc, notMem_uIcc_of_lt, uIcc_of_ge, uIcc_injective_right, NNReal.image_coe_uIcc, uIcc_of_le, Function.Periodic.image_uIcc, image_neg_uIcc, preimage_mul_const_uIcc, isCompact_uIcc, ncard_uIcc_nat, image_div_const_uIcc, unitInterval.volume_uIcc, closure_uIoc, Antitone.image_uIcc_subset, Fin.preimage_val_uIcc_val, intervalIntegral.FTCFilter.nhdsUIcc, Fin.preimage_castSucc_uIcc_castSucc, notMem_uIcc_of_gt, image_mulSingle_uIcc, Fin.preimage_succ_uIcc_succ, intervalIntegrable_sub_inv_iff, right_mem_uIcc, image_sub_const_uIcc, monotoneOn_or_antitoneOn_iff_uIcc, uIcc_subset_uIcc_iff_le', uIoc_subset_uIcc, ContinuousOn.surjOn_uIcc, PNat.card_fintype_uIcc, image_mul_const_uIcc, uIcc_subset_uIcc_union_uIcc, uIcc_self, Rat.preimage_cast_uIcc, bdd_below_bdd_above_iff_subset_uIcc, AbsolutelyContinuousOnInterval.uniformContinuousOn, left_mem_uIcc, uIcc_ofDual, Monotone.image_uIcc_subset, uIcc_subset_Icc, NNRat.preimage_cast_uIcc, image_const_add_uIcc, Path.range_subpath, AffineMap.image_uIcc, uIcc_toDual, monotone_or_antitone_iff_uIcc, continuousOn_uIcc_extendFrom_uIoo, OrderEmbedding.preimage_uIcc, Fin.preimage_natAdd_uIcc_natAdd, uIcc_eq_union, uIcc_subset_uIcc_iff_le, image_mulSingle_uIcc_right, isPreconnected_uIcc, convex_uIcc, uIoo_subset_uIcc, measurableSet_uIcc, uIoo_subset_uIcc_self, preimage_const_mul_uIcc, Real.volume_real_interval, image_const_sub_uIcc, pi_univ_uIcc, inv_uIcc, Filter.tendsto_Ioc_uIcc_uIcc, preimage_const_sub_uIcc, Fin.image_addNat_uIcc, image_add_const_uIcc, Filter.tendsto_Icc_uIcc_uIcc, image_single_uIcc_left, image_update_uIcc_left, Fin.image_succ_uIcc, Continuous.integrableOn_uIcc, Fin.image_val_uIcc, Fintype.card_uIcc, AbsolutelyContinuousOnInterval.uniformlyContinuousOn, image_single_uIcc, Icc_subset_uIcc', nonempty_uIcc, ordConnected_iff_uIcc_subset_right, Monotone.mapsTo_uIcc, Fin.image_natAdd_uIcc, segment_subset_uIcc, quasilinearOn_iff_mem_uIcc, image_update_uIcc, image_update_uIcc_right, preimage_sub_const_uIcc, uIcc_prod_eq, preimage_div_const_uIcc, finite_interval, Fin.preimage_castAdd_uIcc_castAdd, Fin.preimage_cast_uIcc, ordConnected_iff_uIcc_subset, ordConnectedProj_eq, Fin.preimage_rev_uIcc, uIcc_of_gt, MeasureTheory.uIoc_ae_eq_interval, Filter.tendsto_uIcc_of_Icc, Fin.image_castLE_uIcc, AbsolutelyContinuousOnInterval.continuousOn, preimage_const_add_uIcc, ENNReal.image_coe_uIcc, mem_uIcc_of_ge, intervalIntegrable_inv_iff, mem_ordConnectedComponent, uIcc_of_not_le, Complex.horizontalSegment_eq, Finset.coe_uIcc, image_subtype_val_uIcc, Real.volume_interval, parallelepiped_single, mem_uIcc, Fin.preimage_castLE_uIcc_castLE, ordConnected_uIcc, Fin.image_castAdd_uIcc
|
uIoc π | CompOp | 78 mathmath: OrdConnected.uIoc_subset, intervalIntegrable_iff, intervalIntegral.intervalIntegral_eq_integral_uIoc, Fin.image_addNat_uIoc, nonempty_uIoc, interval_average_eq_div, exists_eq_interval_average_of_noAtoms, Fin.image_castLE_uIoc, OrderEmbedding.preimage_uIoc, Ioc_subset_uIoc', Fin.preimage_castSucc_uIoc_castSucc, NNReal.image_coe_uIoc, Fin.preimage_castLE_uIoc_castLE, ENNReal.image_coe_uIoc, Fin.preimage_natAdd_uIoc_natAdd, curveIntegralFun_trans_aeeq_right, AbsolutelyContinuousOnInterval.tendsto_volume_totalLengthFilter_nhds_zero, intervalIntegral.abs_intervalIntegral_eq, uIoc_union_uIoc, uIoc_comm, Fin.preimage_addNat_uIoc_addNat, closure_uIoc, intervalIntegral.integral_cases, right_mem_uIoc, Ioc_subset_uIoc, interval_average_symm, uIoc_subset_uIcc, uIoc_injective_right, measurableSet_uIoc, left_mem_uIoc, intervalIntegral.norm_intervalIntegral_eq, image_subtype_val_uIoc, AbsolutelyContinuousOnInterval.tendsto_volume_restrict_totalLengthFilter_disjWithin_nhds_zero, aemeasurable_uIoc_iff, AbsolutelyContinuousOnInterval.biUnion_uIoc_subset_of_mem_disjWithin, intervalIntegrable_const_iff, Continuous.integrableOn_uIoc, Rat.preimage_cast_uIoc, Fin.image_castAdd_uIoc, uIoc_subset_uIoc_of_uIcc_subset_uIcc, MeasureTheory.ae_restrict_uIoc_iff, uIoc_injective_left, Fin.preimage_cast_uIoc, Fin.preimage_succ_uIoc_succ, Fin.preimage_val_uIoc_val, injOn_circleMap_of_abs_sub_le, mem_uIoc, exists_eq_interval_average_of_measure, isPreconnected_uIoc, Real.circleAverage_eq_intervalAverage, IntervalIntegrable.def', intervalIntegral.abs_integral_eq_abs_integral_uIoc, AbsolutelyContinuousOnInterval.uIoc_subset_of_mem_disjWithin, curveIntegralFun_trans_aeeq_left, intervalIntegral.norm_integral_eq_norm_integral_uIoc, Fin.image_val_uIoc, IntervalIntegrable.aestronglyMeasurable_restrict_uIoc, Fin.preimage_castAdd_uIoc_castAdd, Real.volume_uIoc, unitInterval.volume_uIoc, interval_average_eq, strictConvex_uIoc, exists_eq_interval_average, isConnected_uIoc, MeasureTheory.uIoc_ae_eq_interval, Fin.image_succ_uIoc, MeasureTheory.ae_restrict_uIoc_eq, intervalIntegral.norm_integral_le_integral_norm_uIoc, uIoc_of_le, integral_pow_abs_sub_uIoc, Fin.image_natAdd_uIoc, uIoc_of_ge, uIoc_eq_union, ordConnected_uIoc, NNRat.preimage_cast_uIoc, notMem_uIoc, Fin.image_castSucc_uIoc, MeasureTheory.AEStronglyMeasurable.aestronglyMeasurable_uIoc_iff
|
uIoo π | CompOp | 53 mathmath: right_notMem_uIoo, Fin.preimage_castSucc_uIoo_castSucc, isPreconnected_uIoo, nhdsWithin_uIoo_right_le_nhdsNE, uIoo_subset_Ioo, Fin.preimage_natAdd_uIoo_natAdd, exists_eq_interval_average_of_noAtoms, mem_uIoo_of_gt, Fin.image_succ_uIoo, uIoo_of_ge, uIoo_eq_union, closure_uIoo, uIoo_of_not_ge, nonempty_uIoo, Ioo_min_max, Fin.image_val_uIoo, unitInterval.volume_uIoo, uIoo_of_lt, Fin.preimage_cast_uIoo, uIoo_toDual, image_subtype_val_uIoo, Fin.preimage_castAdd_uIoo_castAdd, Ioo_subset_uIoo, ENNReal.image_coe_uIoo, Fin.preimage_val_uIoo_val, mem_uIoo_of_lt, exists_isLocalExtr_uIoo, Fin.image_castLE_uIoo, uIoo_subset_uIcc, Fin.image_castAdd_uIoo, uIoo_subset_uIcc_self, uIoo_of_not_le, uIoo_comm, Fin.image_castSucc_uIoo, Fin.image_natAdd_uIoo, nhdsWithin_uIoo_left_le_nhdsNE, Real.volume_uIoo, exists_rat_mem_uIoo, Fin.image_addNat_uIoo, left_notMem_uIoo, uIoo_ofDual, Fin.preimage_addNat_uIoo_addNat, uIoo_of_gt, Fin.preimage_rev_uIoo, uIoo_self, uIoo_of_le, exists_eq_interval_average, isConnected_uIoo, Fin.preimage_castLE_uIoo_castLE, exists_uIoo_isExtrOn_uIcc, NNReal.image_coe_uIoo, Ioo_subset_uIoo', Fin.preimage_succ_uIoo_succ
|