| Name | Category | Theorems |
|---|
LowerHemicontinuous 📖 | MathDef | 10 mathmath: isOpenMap_iff_lowerHemicontinuous, lowerHemicontinuous_iff, lowerHemicontinuous_iff_isOpen_compl_preimage_Iic_compl, LowerHemicontinuous.const, lowerHemicontinuous_restrict_iff, LowerHemicontinuous.of_frequently, lowerHemicontinuous_iff_isClosed_preimage_Iic, lowerHemicontinuousOn_univ_iff, LowerHemicontinuous.comp, lowerHemicontinuous_iff_frequently
|
LowerHemicontinuousAt 📖 | MathDef | 8 mathmath: LowerHemicontinuousAt.const, lowerHemicontinuous_iff, LowerHemicontinuousAt.comp, LowerHemicontinuousAt.of_frequently, lowerHemicontinuousAt_iff, lowerHemicontinuousAt_iff_frequently, LowerHemicontinuous.lowerHemicontinuousAt, lowerHemicontinuousWithinAt_univ_iff
|
LowerHemicontinuousOn 📖 | MathDef | 9 mathmath: LowerHemicontinuousOn.const, LowerHemicontinuous.lowerHemicontinuousOn, LowerHemicontinuousOn.of_frequently, lowerHemicontinuous_restrict_iff, lowerHemicontinuousOn_iff_frequently, lowerHemicontinuousOn_univ_iff, LowerHemicontinuousOn.mono, LowerHemicontinuousOn.comp, lowerHemicontinuousOn_iff
|
LowerHemicontinuousWithinAt 📖 | MathDef | 12 mathmath: lowerHemicontinuousWithinAt_iff_frequently, LowerHemicontinuousWithinAt.comp, LowerHemicontinuousOn.lowerHemicontinuousWithinAt, LowerHemicontinuousWithinAt.const, LowerHemicontinuous.lowerHemicontinuousWithinAt, LowerHemicontinuousWithinAt.mono, LowerHemicontinuousAt.lowerHemicontinuousWithinAt, LowerHemicontinuousWithinAt.of_frequently, lowerHemicontinuousWithinAt_univ_iff, lowerHemicontinuousOn_iff, LowerHemicontinuousWithinAt.congr_of_eventuallyEq, lowerHemicontinuousWithinAt_iff
|
LowerSemicontinuous 📖 | MathDef | 42 mathmath: MeasureTheory.exists_lt_lowerSemicontinuous_integral_gt_nnreal, lowerSemicontinuous_ciSup, upperSemiContinuous_inv_iff, upperSemiContinuous_neg_iff, lowerSemicontinuous_iff_isClosed_preimage, LowerSemicontinuous.add, MeasureTheory.exists_lt_lowerSemicontinuous_lintegral_ge_of_aemeasurable, MeasureTheory.exists_le_lowerSemicontinuous_lintegral_ge, lowerSemicontinuous_iff_le_liminf, MeasureTheory.exists_lt_lowerSemicontinuous_lintegral_ge, IsClosed.lowerSemicontinuous_indicator, continuous_iff_lower_upperSemicontinuous, IsOpen.lowerSemicontinuous_indicator, lowerSemicontinuous_iff_frequently, lowerSemicontinuous_sum, Continuous.comp_lowerSemicontinuous, lowerSemicontinuous_iff_isClosed_epigraph, LowerSemicontinuous.inf, lowerSemicontinuous_iSup, LowerSemicontinuous.sup, lowerSemiContinuous_inv_iff, MeasureTheory.exists_lt_lowerSemicontinuous_integral_lt, LowerSemicontinuous.comp_continuous, MeasureTheory.SimpleFunc.exists_le_lowerSemicontinuous_lintegral_ge, lowerSemicontinuous_restrict_iff, eVariationOn.lowerSemicontinuous_uniformOn, lowerSemicontinuous_const, EReal.lowerSemicontinuous_add, LowerSemicontinuous.comp, lowerSemiContinuous_neg_iff, LowerSemicontinuous.add', lowerSemicontinuous_iff, Continuous.lowerSemicontinuous, lowerSemicontinuousOn_univ_iff, UpperSemicontinuous.neg, Continuous.comp_upperSemicontinuous_antitone, lowerSemicontinuous_iff_isOpen_preimage, LowerSemicontinuous.of_frequently, lowerSemicontinuous_tsum, eVariationOn.lowerSemicontinuous, UpperSemicontinuous.inv, lowerSemicontinuous_biSup
|
LowerSemicontinuousAt 📖 | MathDef | 32 mathmath: LowerSemicontinuousAt.of_frequently, LowerSemicontinuousAt.comp_continuousAt, lowerSemicontinuousAt_const, upperSemicontinuousAt_neg_iff, ContinuousAt.comp_lowerSemicontinuousAt, IsClosed.lowerSemicontinuousAt_indicator, LowerSemicontinuousAt.comp, lowerSemicontinuousWithinAt_univ_iff, LowerSemicontinuousAt.sup, lowerSemicontinuousAt_sum, LowerSemicontinuousAt.inf, upperSemicontinuousAt_inv_iff, ContinuousAt.comp_upperSemicontinuousAt_antitone, UpperSemicontinuousAt.inv, LowerSemicontinuousAt.add, lowerSemicontinuouAt_neg_iff, lowerSemicontinuousAt_tsum, lowerSemicontinuousAt_iff_le_liminf, lowerSemicontinuousAt_iff_frequently, UpperSemicontinuousAt.neg, LowerSemicontinuousAt.comp_continuousAt_of_eq, lowerSemicontinuous_iff, lowerSemicontinuousAt_iSup, LowerSemicontinuous.lowerSemicontinuousAt, LowerSemicontinuousAt.add', ContinuousAt.lowerSemicontinuousAt, lowerSemicontinuousAt_biSup, lowerSemicontinuousAt_iff, lowerSemicontinuousAt_ciSup, lowerSemicontinuouAt_inv_iff, continuousAt_iff_lower_upperSemicontinuousAt, IsOpen.lowerSemicontinuousAt_indicator
|
LowerSemicontinuousOn 📖 | MathDef | 34 mathmath: lowerSemicontinuousOn_biSup, LowerSemicontinuousOn.add, lowerSemicontinuousOn_const, lowerSemicontinuousOn_iSup, lowerSemicontinuousOn_neg_iff, lowerSemicontinuousOn_iff_preimage_Ioi, upperSemicontinuousOn_inv_iff, IsOpen.lowerSemicontinuousOn_indicator, lowerSemicontinuousOn_iff_isClosed_epigraph, lowerSemicontinuousOn_sum, lowerSemicontinuousOn_tsum, LowerSemicontinuousOn.add', continuousOn_iff_lower_upperSemicontinuousOn, UpperSemicontinuousOn.neg, LowerSemicontinuousOn.of_frequently, LowerSemicontinuousOn.inf, LowerSemicontinuous.lowerSemicontinuousOn, lowerSemicontinuousOn_iff_frequently, UpperSemicontinuousOn.inv, Continuous.comp_upperSemicontinuousOn_antitone, lowerSemicontinuous_restrict_iff, ContinuousOn.lowerSemicontinuousOn, lowerSemicontinuousOn_iff_preimage_Iic, upperSemicontinuousOn_neg_iff, LowerSemicontinuousOn.mono, lowerSemicontinuousOn_ciSup, LowerSemicontinuousOn.comp, lowerSemicontinuousOn_univ_iff, lowerSemicontinuousOn_iff, LowerSemicontinuousOn.sup, IsClosed.lowerSemicontinuousOn_indicator, Continuous.comp_lowerSemicontinuousOn, lowerSemicontinuousOn_iff_le_liminf, lowerSemicontinuousOn_inv_iff
|
LowerSemicontinuousWithinAt 📖 | MathDef | 34 mathmath: UpperSemicontinuousWithinAt.inv, lowerSemicontinuousWithinAt_iSup, LowerSemicontinuousWithinAt.of_frequently, upperSemicontinuousWithinAt_neg_iff, LowerSemicontinuousWithinAt.mono, UpperSemicontinuousWithinAt.neg, lowerSemicontinuousWithinAt_tsum, LowerSemicontinuousWithinAt.comp, continuousWithinAt_iff_lower_upperSemicontinuousWithinAt, LowerSemicontinuousWithinAt.add, lowerSemicontinuousWithinAt_univ_iff, LowerSemicontinuousWithinAt.sup, LowerSemicontinuous.lowerSemicontinuousWithinAt, LowerSemicontinuousWithinAt.inf, IsOpen.lowerSemicontinuousWithinAt_indicator, lowerSemicontinuousWithinAt_inv_iff, lowerSemicontinuousWithinAt_ciSup, ContinuousWithinAt.lowerSemicontinuousWithinAt, LowerSemicontinuousWithinAt.add', ContinuousAt.comp_lowerSemicontinuousWithinAt, LowerSemicontinuousOn.lowerSemicontinuousWithinAt, lowerSemicontinuousWithinAt_iff, lowerSemicontinuousWithinAt_iff_le_liminf, ContinuousAt.comp_upperSemicontinuousWithinAt_antitone, upperSemicontinuousWithinAt_inv_iff, LowerSemicontinuousWithinAt.congr_of_eventuallyEq, lowerSemicontinuousWithinAt_sum, lowerSemicontinuousWithinAt_const, LowerSemicontinuousAt.lowerSemicontinuousWithinAt, IsClosed.lowerSemicontinuousWithinAt_indicator, lowerSemicontinuousWithinAt_biSup, lowerSemicontinuousOn_iff, lowerSemicontinuousWithinAt_iff_frequently, lowerSemicontinuousWithinAt_neg_iff
|
SemicontinuousAt 📖 | MathDef | 5 mathmath: semicontinuousWithinAt_univ_iff, Semicontinuous.semicontinuousAt, SemicontinuousAt.const, semicontinuousAt_iff_frequently, SemicontinuousAt.comp
|
SemicontinuousOn 📖 | MathDef | 7 mathmath: semicontinuousOn_univ_iff, semicontinuous_restrict_iff, SemicontinuousOn.const, Semicontinuous.semicontinuousOn, SemicontinuousOn.mono, SemicontinuousOn.comp, semicontinuousOn_iff_frequently
|
SemicontinuousWithinAt 📖 | MathDef | 9 mathmath: SemicontinuousWithinAt.congr_of_eventuallyEq, semicontinuousWithinAt_univ_iff, Semicontinuous.semicontinuousWithinAt, semicontinuousWithinAt_iff_frequently, SemicontinuousWithinAt.const, SemicontinuousAt.semicontinuousWithinAt, SemicontinuousWithinAt.comp, SemicontinuousOn.semicontinuousWithinAt, SemicontinuousWithinAt.mono
|
UpperHemicontinuous 📖 | MathDef | 22 mathmath: UpperHemicontinuous.of_forall_isOpen, UpperHemicontinuous.of_frequently, upperHemicontinuous_singleton_id, upperHemicontinuousOn_univ_iff, upperHemicontinuous_iff_frequently, upperHemicontinuous_quasispectrum, upperHemicontinuous_iff_isOpen_preimage_Iic, upperHemicontinuous_iff_preimage_Iic, UpperHemicontinuous.inter, upperHemicontinuous_spectrum_nnreal, UpperHemicontinuous.comp, upperHemicontinuous_quasispectrum_nnreal, upperHemicontinuous_singleton_iff, upperHemicontinuous_iff, upperHemicontinuous_iff_isClosed_compl_preimage_Iic_compl, UpperHemicontinuous.isInducing_comp, upperHemicontinuousOn_iff_restrict, UpperHemicontinuous.union, UpperHemicontinuous.const, upperHemicontinuous_spectrum, isClosedMap_iff_upperHemicontinuous, upperHemicontinuous_iff_forall_isOpen
|
UpperHemicontinuousAt 📖 | MathDef | 16 mathmath: upperHemicontinuousAt_iff_forall_isOpen, UpperHemicontinuousAt.inter, UpperHemicontinuousAt.comp, upperHemicontinuousAt_singleton_iff, UpperHemicontinuousAt.isInducing_comp, upperHemicontinuousAt_iff_preimage_Iic, UpperHemicontinuousAt.const, UpperHemicontinuousAt.of_sequences, UpperHemicontinuousAt.union, upperHemicontinuousAt_iff, UpperHemicontinuousAt.of_forall_isOpen, upperHemicontinuous_iff, UpperHemicontinuousAt.of_frequently, UpperHemicontinuous.upperHemicontinuousAt, upperHemicontinuousWithinAt_univ_iff, upperHemicontinuousAt_iff_frequently
|
UpperHemicontinuousOn 📖 | MathDef | 16 mathmath: UpperHemicontinuousOn.of_frequently, UpperHemicontinuousOn.of_forall_isOpen, UpperHemicontinuousOn.union, UpperHemicontinuous.upperHemicontinuousOn, upperHemicontinuousOn_iff_frequently, UpperHemicontinuousOn.const, upperHemicontinuousOn_iff_preimage_Iic, UpperHemicontinuousOn.inter, upperHemicontinuousOn_univ_iff, upperHemicontinuousOn_iff_forall_isOpen, UpperHemicontinuousOn.comp, UpperHemicontinuousOn.mono, UpperHemicontinuousOn.isInducing_comp, upperHemicontinuousOn_singleton_iff, upperHemicontinuousOn_iff, upperHemicontinuousOn_iff_restrict
|
UpperHemicontinuousWithinAt 📖 | MathDef | 19 mathmath: upperHemicontinuousWithinAt_iff_frequently, UpperHemicontinuousWithinAt.inter, upperHemicontinuousWithinAt_iff_forall_isOpen, UpperHemicontinuousAt.upperHemicontinuousWithinAt, upperHemicontinuousWithinAt_iff_preimage_Iic, UpperHemicontinuousWithinAt.isInducing_comp, UpperHemicontinuous.upperHemicontinuousWithinAt, UpperHemicontinuousWithinAt.of_frequently, UpperHemicontinuousWithinAt.congr_of_eventuallyEq, UpperHemicontinuousWithinAt.comp, upperHemicontinuousWithinAt_iff, UpperHemicontinuousOn.upperHemicontinuousWithinAt, UpperHemicontinuousWithinAt.const, UpperHemicontinuousWithinAt.mono, upperHemicontinuousOn_iff, upperHemicontinuousWithinAt_singleton_iff, upperHemicontinuousWithinAt_univ_iff, UpperHemicontinuousWithinAt.union, UpperHemicontinuousWithinAt.of_forall_isOpen
|
UpperSemicontinuous 📖 | MathDef | 36 mathmath: UpperSemicontinuous.add', LowerSemicontinuous.neg, UpperSemicontinuous.comp, upperSemiContinuous_inv_iff, Continuous.upperSemicontinuous, LowerSemicontinuous.inv, upperSemiContinuous_neg_iff, MeasureTheory.exists_upperSemicontinuous_le_lintegral_le, upperSemicontinuous_biInf, continuous_iff_lower_upperSemicontinuous, upperSemicontinuous_iff, UpperSemicontinuous.of_frequently, upperSemicontinuous_iff_frequently, upperSemicontinuous_ciInf, IsClosed.upperSemicontinuous_indicator, upperSemicontinuous_const, Continuous.comp_upperSemicontinuous, Continuous.comp_lowerSemicontinuous_antitone, upperSemicontinuous_iInf, lowerSemiContinuous_inv_iff, UpperSemicontinuous.comp_continuous, upperSemicontinuous_iff_limsup_le, UpperSemicontinuous.sup, UpperSemicontinuous.add, upperSemicontinuous_iff_isClosed_preimage, upperSemicontinuous_sum, upperSemicontinuous_iff_IsClosed_hypograph, upperSemicontinuous_iff_isOpen_preimage, MeasureTheory.SimpleFunc.exists_upperSemicontinuous_le_lintegral_le, lowerSemiContinuous_neg_iff, IsOpen.upperSemicontinuous_indicator, MeasureTheory.exists_upperSemicontinuous_le_integral_le, MeasureTheory.exists_upperSemicontinuous_lt_integral_gt, UpperSemicontinuous.inf, upperSemicontinuousOn_iff_restrict, upperSemicontinuousOn_univ_iff
|
UpperSemicontinuousAt 📖 | MathDef | 31 mathmath: upperSemicontinuousAt_biInf, upperSemicontinuousAt_iff_frequently, upperSemicontinuousAt_neg_iff, ContinuousAt.comp_lowerSemicontinuousAt_antitone, ContinuousAt.comp_upperSemicontinuousAt, upperSemicontinuous_iff, upperSemicontinuousAt_sum, upperSemicontinuousAt_inv_iff, upperSemicontinuousAt_iff_limsup_le, lowerSemicontinuouAt_neg_iff, UpperSemicontinuousAt.comp, upperSemicontinuousAt_iff, upperSemicontinuousWithinAt_univ_iff, UpperSemicontinuousAt.add, IsClosed.upperSemicontinuousAt_indicator, upperSemicontinuousAt_ciInf, IsOpen.upperSemicontinuousAt_indicator, UpperSemicontinuousAt.sup, UpperSemicontinuousAt.of_frequently, UpperSemicontinuous.upperSemicontinuousAt, UpperSemicontinuousAt.inf, LowerSemicontinuousAt.neg, upperSemicontinuousAt_iInf, UpperSemicontinuousAt.add', upperSemicontinuousAt_const, UpperSemicontinuousAt.comp_continuousAt_of_eq, ContinuousAt.upperSemicontinuousAt, LowerSemicontinuousAt.inv, lowerSemicontinuouAt_inv_iff, continuousAt_iff_lower_upperSemicontinuousAt, UpperSemicontinuousAt.comp_continuousAt
|
UpperSemicontinuousOn 📖 | MathDef | 33 mathmath: LowerSemicontinuousOn.inv, Continuous.comp_lowerSemicontinuousOn_antitone, lowerSemicontinuousOn_neg_iff, UpperSemicontinuousOn.add', upperSemicontinuousOn_inv_iff, upperSemicontinuousOn_iInf, upperSemicontinuousOn_iff_limsup_le, upperSemicontinuousOn_iff_preimage_Iio, ContinuousOn.upperSemicontinuousOn, continuousOn_iff_lower_upperSemicontinuousOn, upperSemicontinuousOn_const, UpperSemicontinuousOn.add, Continuous.comp_upperSemicontinuousOn, upperSemicontinuousOn_iff_frequently, UpperSemicontinuousOn.of_frequently, upperSemicontinuousOn_ciInf, LowerSemicontinuousOn.neg, UpperSemicontinuousOn.sup, UpperSemicontinuousOn.comp, upperSemicontinuousOn_biInf, IsOpen.upperSemicontinuousOn_indicator, upperSemicontinuousOn_sum, upperSemicontinuousOn_neg_iff, UpperSemicontinuous.upperSemicontinuousOn, upperSemicontinuousOn_iff_isClosed_hypograph, UpperSemicontinuousOn.mono, upperSemicontinuousOn_iff_restrict, IsClosed.upperSemicontinuousOn_indicator, upperSemicontinuousOn_iff_preimage_Ici, lowerSemicontinuousOn_inv_iff, UpperSemicontinuousOn.inf, upperSemicontinuousOn_iff, upperSemicontinuousOn_univ_iff
|
UpperSemicontinuousWithinAt 📖 | MathDef | 33 mathmath: LowerSemicontinuousWithinAt.neg, ContinuousAt.comp_lowerSemicontinuousWithinAt_antitone, UpperSemicontinuousWithinAt.mono, ContinuousAt.comp_upperSemicontinuousWithinAt, LowerSemicontinuousWithinAt.inv, upperSemicontinuousWithinAt_neg_iff, IsClosed.upperSemicontinuousWithinAt_indicator, UpperSemicontinuousWithinAt.add, upperSemicontinuousWithinAt_sum, continuousWithinAt_iff_lower_upperSemicontinuousWithinAt, UpperSemicontinuousAt.upperSemicontinuousWithinAt, UpperSemicontinuous.upperSemicontinuousWithinAt, upperSemicontinuousWithinAt_const, upperSemicontinuousWithinAt_iff_limsup_le, IsOpen.upperSemicontinuousWithinAt_indicator, UpperSemicontinuousOn.upperSemicontinuousWithinAt, UpperSemicontinuousWithinAt.congr_of_eventuallyEq, lowerSemicontinuousWithinAt_inv_iff, upperSemicontinuousWithinAt_inv_iff, upperSemicontinuousWithinAt_univ_iff, upperSemicontinuousWithinAt_biInf, UpperSemicontinuousWithinAt.sup, upperSemicontinuousWithinAt_iff, UpperSemicontinuousWithinAt.add', UpperSemicontinuousWithinAt.of_frequently, upperSemicontinuousWithinAt_iInf, UpperSemicontinuousWithinAt.comp, UpperSemicontinuousWithinAt.inf, ContinuousWithinAt.upperSemicontinuousWithinAt, upperSemicontinuousWithinAt_ciInf, lowerSemicontinuousWithinAt_neg_iff, upperSemicontinuousWithinAt_iff_frequently, upperSemicontinuousOn_iff
|