Defs

📁 Source: Mathlib/Topology/Semicontinuity/Defs.lean

Statistics

Metric	Count
Definitions `LowerHemicontinuous`, `LowerHemicontinuousAt`, `LowerHemicontinuousOn`, `LowerHemicontinuousWithinAt`, `LowerSemicontinuous`, `LowerSemicontinuousAt`, `LowerSemicontinuousOn`, `LowerSemicontinuousWithinAt`, `SemicontinuousAt`, `SemicontinuousOn`, `SemicontinuousWithinAt`, `UpperHemicontinuous`, `UpperHemicontinuousAt`, `UpperHemicontinuousOn`, `UpperHemicontinuousWithinAt`, `UpperSemicontinuous`, `UpperSemicontinuousAt`, `UpperSemicontinuousOn`, `UpperSemicontinuousWithinAt`	19
Theorems `comp`, `const`, `frequently`, `lowerHemicontinuousAt`, `lowerHemicontinuousOn`, `lowerHemicontinuousWithinAt`, `of_frequently`, `comp`, `const`, `frequently`, `lowerHemicontinuousWithinAt`, `of_frequently`, `comp`, `const`, `frequently`, `lowerHemicontinuousWithinAt`, `mono`, `of_frequently`, `comp`, `congr_of_eventuallyEq`, `const`, `frequently`, `mono`, `of_frequently`, `comp`, `frequently`, `lowerSemicontinuousAt`, `lowerSemicontinuousOn`, `lowerSemicontinuousWithinAt`, `of_frequently`, `comp`, `frequently`, `lowerSemicontinuousWithinAt`, `of_frequently`, `comp`, `frequently`, `lowerSemicontinuousWithinAt`, `mono`, `of_frequently`, `comp`, `congr_of_eventuallyEq`, `frequently`, `mono`, `of_frequently`, `comp`, `const`, `semicontinuousAt`, `semicontinuousOn`, `semicontinuousWithinAt`, `comp`, `const`, `semicontinuousWithinAt`, `comp`, `const`, `mono`, `semicontinuousWithinAt`, `comp`, `congr_of_eventuallyEq`, `const`, `mono`, `comp`, `const`, `frequently`, `of_frequently`, `upperHemicontinuousAt`, `upperHemicontinuousOn`, `upperHemicontinuousWithinAt`, `comp`, `const`, `frequently`, `of_frequently`, `upperHemicontinuousWithinAt`, `comp`, `const`, `frequently`, `mono`, `of_frequently`, `upperHemicontinuousWithinAt`, `comp`, `congr_of_eventuallyEq`, `const`, `frequently`, `mono`, `of_frequently`, `comp`, `frequently`, `of_frequently`, `upperSemicontinuousAt`, `upperSemicontinuousOn`, `upperSemicontinuousWithinAt`, `comp`, `frequently`, `of_frequently`, `upperSemicontinuousWithinAt`, `comp`, `frequently`, `mono`, `of_frequently`, `upperSemicontinuousWithinAt`, `comp`, `congr_of_eventuallyEq`, `frequently`, `mono`, `of_frequently`, `lowerHemicontinuousAt_iff`, `lowerHemicontinuousAt_iff_frequently`, `lowerHemicontinuousOn_iff`, `lowerHemicontinuousOn_iff_frequently`, `lowerHemicontinuousOn_univ_iff`, `lowerHemicontinuousWithinAt_iff`, `lowerHemicontinuousWithinAt_iff_frequently`, `lowerHemicontinuousWithinAt_univ_iff`, `lowerHemicontinuous_iff`, `lowerHemicontinuous_iff_frequently`, `lowerHemicontinuous_restrict_iff`, `lowerSemicontinuousAt_const`, `lowerSemicontinuousAt_iff`, `lowerSemicontinuousAt_iff_frequently`, `lowerSemicontinuousOn_const`, `lowerSemicontinuousOn_iff`, `lowerSemicontinuousOn_iff_frequently`, `lowerSemicontinuousOn_univ_iff`, `lowerSemicontinuousWithinAt_const`, `lowerSemicontinuousWithinAt_iff`, `lowerSemicontinuousWithinAt_iff_frequently`, `lowerSemicontinuousWithinAt_univ_iff`, `lowerSemicontinuous_const`, `lowerSemicontinuous_iff`, `lowerSemicontinuous_iff_frequently`, `lowerSemicontinuous_restrict_iff`, `semicontinuousAt_iff_frequently`, `semicontinuousOn_iff_frequently`, `semicontinuousOn_univ_iff`, `semicontinuousWithinAt_iff_frequently`, `semicontinuousWithinAt_univ_iff`, `semicontinuous_iff_frequently`, `semicontinuous_restrict_iff`, `upperHemicontinuousAt_iff`, `upperHemicontinuousAt_iff_frequently`, `upperHemicontinuousOn_iff`, `upperHemicontinuousOn_iff_frequently`, `upperHemicontinuousOn_iff_restrict`, `upperHemicontinuousOn_univ_iff`, `upperHemicontinuousWithinAt_iff`, `upperHemicontinuousWithinAt_iff_frequently`, `upperHemicontinuousWithinAt_univ_iff`, `upperHemicontinuous_iff`, `upperHemicontinuous_iff_frequently`, `upperSemicontinuousAt_const`, `upperSemicontinuousAt_iff`, `upperSemicontinuousAt_iff_frequently`, `upperSemicontinuousOn_const`, `upperSemicontinuousOn_iff`, `upperSemicontinuousOn_iff_frequently`, `upperSemicontinuousOn_iff_restrict`, `upperSemicontinuousOn_univ_iff`, `upperSemicontinuousWithinAt_const`, `upperSemicontinuousWithinAt_iff`, `upperSemicontinuousWithinAt_iff_frequently`, `upperSemicontinuousWithinAt_univ_iff`, `upperSemicontinuous_const`, `upperSemicontinuous_iff`, `upperSemicontinuous_iff_frequently`	163
Total	182

LowerHemicontinuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	mathematical	`LowerHemicontinuous` `Continuous`	`Set`	—	`Semicontinuous.comp`
`const` 📖	mathematical	—	`LowerHemicontinuous`	—	`Semicontinuous.const`
`frequently` 📖	—	`LowerHemicontinuous` `Filter.Frequently` `Set` `Set.instHasSubset` `nhds`	—	—	`lowerHemicontinuous_iff_frequently`
`lowerHemicontinuousAt` 📖	mathematical	`LowerHemicontinuous`	`LowerHemicontinuousAt`	—	—
`lowerHemicontinuousOn` 📖	mathematical	`LowerHemicontinuous`	`LowerHemicontinuousOn`	—	`Semicontinuous.semicontinuousOn`
`lowerHemicontinuousWithinAt` 📖	mathematical	`LowerHemicontinuous`	`LowerHemicontinuousWithinAt`	—	`SemicontinuousAt.semicontinuousWithinAt`
`of_frequently` 📖	mathematical	`Set` `Set.instHasSubset`	`LowerHemicontinuous`	—	`lowerHemicontinuous_iff_frequently`

LowerHemicontinuousAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	mathematical	`LowerHemicontinuousAt` `ContinuousAt`	`Set`	—	`SemicontinuousAt.comp`
`const` 📖	mathematical	—	`LowerHemicontinuousAt`	—	`SemicontinuousAt.const`
`frequently` 📖	—	`LowerHemicontinuousAt` `Filter.Frequently` `Set` `Set.instHasSubset` `nhds`	—	—	`lowerHemicontinuousAt_iff_frequently`
`lowerHemicontinuousWithinAt` 📖	mathematical	`LowerHemicontinuousAt`	`LowerHemicontinuousWithinAt`	—	`SemicontinuousAt.semicontinuousWithinAt`
`of_frequently` 📖	mathematical	`Set` `Set.instHasSubset`	`LowerHemicontinuousAt`	—	`lowerHemicontinuousAt_iff_frequently`

LowerHemicontinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	mathematical	`LowerHemicontinuousOn` `ContinuousOn` `Set.MapsTo`	`Set`	—	`SemicontinuousOn.comp`
`const` 📖	mathematical	—	`LowerHemicontinuousOn`	—	`SemicontinuousOn.const`
`frequently` 📖	—	`LowerHemicontinuousOn` `Set` `Set.instMembership` `Filter.Frequently` `Set.instHasSubset` `nhdsWithin`	—	—	`lowerHemicontinuousOn_iff_frequently`
`lowerHemicontinuousWithinAt` 📖	mathematical	`LowerHemicontinuousOn` `Set` `Set.instMembership`	`LowerHemicontinuousWithinAt`	—	`SemicontinuousOn.semicontinuousWithinAt`
`mono` 📖	—	`LowerHemicontinuousOn` `Set` `Set.instHasSubset`	—	—	`SemicontinuousOn.mono`
`of_frequently` 📖	mathematical	`Set` `Set.instHasSubset`	`LowerHemicontinuousOn`	—	`lowerHemicontinuousOn_iff_frequently`

LowerHemicontinuousWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	mathematical	`LowerHemicontinuousWithinAt` `ContinuousWithinAt` `Set.MapsTo`	`Set`	—	`SemicontinuousWithinAt.comp`
`congr_of_eventuallyEq` 📖	—	`LowerHemicontinuousWithinAt` `Set` `Set.instMembership` `Filter.EventuallyEq` `nhdsWithin`	—	—	`SemicontinuousWithinAt.congr_of_eventuallyEq` `Filter.mp_mem` `Filter.univ_mem'`
`const` 📖	mathematical	—	`LowerHemicontinuousWithinAt`	—	`SemicontinuousWithinAt.const`
`frequently` 📖	—	`LowerHemicontinuousWithinAt` `Filter.Frequently` `Set` `Set.instHasSubset` `nhdsWithin`	—	—	`lowerHemicontinuousWithinAt_iff_frequently`
`mono` 📖	—	`LowerHemicontinuousWithinAt` `Set` `Set.instHasSubset`	—	—	`SemicontinuousWithinAt.mono`
`of_frequently` 📖	mathematical	`Set` `Set.instHasSubset`	`LowerHemicontinuousWithinAt`	—	`lowerHemicontinuousWithinAt_iff_frequently`

LowerSemicontinuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	—	`LowerSemicontinuous` `Continuous`	—	—	`Semicontinuous.comp`
`frequently` 📖	—	`LowerSemicontinuous` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Filter.Frequently` `Preorder.toLE` `nhds`	—	—	`lowerSemicontinuous_iff_frequently`
`lowerSemicontinuousAt` 📖	mathematical	`LowerSemicontinuous`	`LowerSemicontinuousAt`	—	—
`lowerSemicontinuousOn` 📖	mathematical	`LowerSemicontinuous`	`LowerSemicontinuousOn`	—	`Semicontinuous.semicontinuousOn`
`lowerSemicontinuousWithinAt` 📖	mathematical	`LowerSemicontinuous`	`LowerSemicontinuousWithinAt`	—	`SemicontinuousAt.semicontinuousWithinAt`
`of_frequently` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`LowerSemicontinuous`	—	`lowerSemicontinuous_iff_frequently`

LowerSemicontinuousAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	—	`LowerSemicontinuousAt` `ContinuousAt`	—	—	`SemicontinuousAt.comp`
`frequently` 📖	—	`LowerSemicontinuousAt` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Filter.Frequently` `Preorder.toLE` `nhds`	—	—	`lowerSemicontinuousAt_iff_frequently`
`lowerSemicontinuousWithinAt` 📖	mathematical	`LowerSemicontinuousAt`	`LowerSemicontinuousWithinAt`	—	`SemicontinuousAt.semicontinuousWithinAt`
`of_frequently` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`LowerSemicontinuousAt`	—	`lowerSemicontinuousAt_iff_frequently`

LowerSemicontinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	—	`LowerSemicontinuousOn` `ContinuousOn` `Set.MapsTo`	—	—	`SemicontinuousOn.comp`
`frequently` 📖	—	`LowerSemicontinuousOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set` `Set.instMembership` `Filter.Frequently` `Preorder.toLE` `nhdsWithin`	—	—	`lowerSemicontinuousOn_iff_frequently`
`lowerSemicontinuousWithinAt` 📖	mathematical	`LowerSemicontinuousOn` `Set` `Set.instMembership`	`LowerSemicontinuousWithinAt`	—	`SemicontinuousOn.semicontinuousWithinAt`
`mono` 📖	—	`LowerSemicontinuousOn` `Set` `Set.instHasSubset`	—	—	`SemicontinuousOn.mono`
`of_frequently` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`LowerSemicontinuousOn`	—	`lowerSemicontinuousOn_iff_frequently`

LowerSemicontinuousWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	—	`LowerSemicontinuousWithinAt` `ContinuousWithinAt` `Set.MapsTo`	—	—	`SemicontinuousWithinAt.comp`
`congr_of_eventuallyEq` 📖	—	`LowerSemicontinuousWithinAt` `Set` `Set.instMembership` `Filter.EventuallyEq` `nhdsWithin`	—	—	`SemicontinuousWithinAt.congr_of_eventuallyEq` `Filter.mp_mem` `Filter.univ_mem'`
`frequently` 📖	—	`LowerSemicontinuousWithinAt` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Filter.Frequently` `Preorder.toLE` `nhdsWithin`	—	—	`lowerSemicontinuousWithinAt_iff_frequently`
`mono` 📖	—	`LowerSemicontinuousWithinAt` `Set` `Set.instHasSubset`	—	—	`SemicontinuousWithinAt.mono`
`of_frequently` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`LowerSemicontinuousWithinAt`	—	`lowerSemicontinuousWithinAt_iff_frequently`

Semicontinuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	—	`Semicontinuous` `Continuous`	—	—	`SemicontinuousAt.comp` `semicontinuousAt` `Continuous.continuousAt`
`const` 📖	mathematical	—	`Semicontinuous`	—	`SemicontinuousAt.const`
`semicontinuousAt` 📖	mathematical	`Semicontinuous`	`SemicontinuousAt`	—	—
`semicontinuousOn` 📖	mathematical	`Semicontinuous`	`SemicontinuousOn`	—	`semicontinuousWithinAt`
`semicontinuousWithinAt` 📖	mathematical	`Semicontinuous`	`SemicontinuousWithinAt`	—	`SemicontinuousAt.semicontinuousWithinAt`

SemicontinuousAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	—	`SemicontinuousAt` `ContinuousAt`	—	—	—
`const` 📖	mathematical	—	`SemicontinuousAt`	—	`Filter.Eventually.of_forall`
`semicontinuousWithinAt` 📖	mathematical	`SemicontinuousAt`	`SemicontinuousWithinAt`	—	`Filter.Eventually.filter_mono` `nhdsWithin_le_nhds`

SemicontinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	—	`SemicontinuousOn` `ContinuousOn` `Set.MapsTo`	—	—	`SemicontinuousWithinAt.comp`
`const` 📖	mathematical	—	`SemicontinuousOn`	—	`SemicontinuousWithinAt.const`
`mono` 📖	—	`SemicontinuousOn` `Set` `Set.instHasSubset`	—	—	`SemicontinuousWithinAt.mono`
`semicontinuousWithinAt` 📖	mathematical	`SemicontinuousOn` `Set` `Set.instMembership`	`SemicontinuousWithinAt`	—	—

SemicontinuousWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	—	`SemicontinuousWithinAt` `ContinuousWithinAt` `Set.MapsTo`	—	—	`ContinuousWithinAt.tendsto_nhdsWithin`
`congr_of_eventuallyEq` 📖	—	`SemicontinuousWithinAt` `Set` `Set.instMembership` `Filter.Eventually` `nhdsWithin`	—	—	`Filter.mp_mem` `Filter.EventuallyEq.eq_of_nhdsWithin` `Filter.univ_mem'`
`const` 📖	mathematical	—	`SemicontinuousWithinAt`	—	`Filter.Eventually.of_forall`
`mono` 📖	—	`SemicontinuousWithinAt` `Set` `Set.instHasSubset`	—	—	`Filter.Eventually.filter_mono` `nhdsWithin_mono`

UpperHemicontinuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	mathematical	`UpperHemicontinuous` `Continuous`	`Set`	—	`Semicontinuous.comp`
`const` 📖	mathematical	—	`UpperHemicontinuous`	—	`Semicontinuous.const`
`frequently` 📖	—	`UpperHemicontinuous` `Filter.Frequently` `Set.Nonempty` `Set` `Set.instInter` `nhds`	—	—	`upperHemicontinuous_iff_frequently`
`of_frequently` 📖	mathematical	`Set.Nonempty` `Set` `Set.instInter`	`UpperHemicontinuous`	—	`upperHemicontinuous_iff_frequently`
`upperHemicontinuousAt` 📖	mathematical	`UpperHemicontinuous`	`UpperHemicontinuousAt`	—	—
`upperHemicontinuousOn` 📖	mathematical	`UpperHemicontinuous`	`UpperHemicontinuousOn`	—	`Semicontinuous.semicontinuousOn`
`upperHemicontinuousWithinAt` 📖	mathematical	`UpperHemicontinuous`	`UpperHemicontinuousWithinAt`	—	`SemicontinuousAt.semicontinuousWithinAt`

UpperHemicontinuousAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	mathematical	`UpperHemicontinuousAt` `ContinuousAt`	`Set`	—	`SemicontinuousAt.comp`
`const` 📖	mathematical	—	`UpperHemicontinuousAt`	—	`SemicontinuousAt.const`
`frequently` 📖	—	`UpperHemicontinuousAt` `Filter.Frequently` `Set.Nonempty` `Set` `Set.instInter` `nhds`	—	—	`upperHemicontinuousAt_iff_frequently`
`of_frequently` 📖	mathematical	`Set.Nonempty` `Set` `Set.instInter`	`UpperHemicontinuousAt`	—	`upperHemicontinuousAt_iff_frequently`
`upperHemicontinuousWithinAt` 📖	mathematical	`UpperHemicontinuousAt`	`UpperHemicontinuousWithinAt`	—	`SemicontinuousAt.semicontinuousWithinAt`

UpperHemicontinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	mathematical	`UpperHemicontinuousOn` `ContinuousOn` `Set.MapsTo`	`Set`	—	`SemicontinuousOn.comp`
`const` 📖	mathematical	—	`UpperHemicontinuousOn`	—	`SemicontinuousOn.const`
`frequently` 📖	—	`UpperHemicontinuousOn` `Set` `Set.instMembership` `Filter.Frequently` `Set.Nonempty` `Set.instInter` `nhdsWithin`	—	—	`upperHemicontinuousOn_iff_frequently`
`mono` 📖	—	`UpperHemicontinuousOn` `Set` `Set.instHasSubset`	—	—	`SemicontinuousOn.mono`
`of_frequently` 📖	mathematical	`Set.Nonempty` `Set` `Set.instInter`	`UpperHemicontinuousOn`	—	`upperHemicontinuousOn_iff_frequently`
`upperHemicontinuousWithinAt` 📖	mathematical	`UpperHemicontinuousOn` `Set` `Set.instMembership`	`UpperHemicontinuousWithinAt`	—	—

UpperHemicontinuousWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	mathematical	`UpperHemicontinuousWithinAt` `ContinuousWithinAt` `Set.MapsTo`	`Set`	—	`SemicontinuousWithinAt.comp`
`congr_of_eventuallyEq` 📖	—	`UpperHemicontinuousWithinAt` `Set` `Set.instMembership` `Filter.Eventually` `nhdsWithin`	—	—	`SemicontinuousWithinAt.congr_of_eventuallyEq` `Filter.mp_mem` `Filter.univ_mem'`
`const` 📖	mathematical	—	`UpperHemicontinuousWithinAt`	—	`SemicontinuousWithinAt.const`
`frequently` 📖	—	`UpperHemicontinuousWithinAt` `Filter.Frequently` `Set.Nonempty` `Set` `Set.instInter` `nhdsWithin`	—	—	`upperHemicontinuousWithinAt_iff_frequently`
`mono` 📖	—	`UpperHemicontinuousWithinAt` `Set` `Set.instHasSubset`	—	—	`SemicontinuousWithinAt.mono`
`of_frequently` 📖	mathematical	`Set.Nonempty` `Set` `Set.instInter`	`UpperHemicontinuousWithinAt`	—	`upperHemicontinuousWithinAt_iff_frequently`

UpperSemicontinuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	—	`UpperSemicontinuous` `Continuous`	—	—	`Semicontinuous.comp`
`frequently` 📖	—	`UpperSemicontinuous` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Filter.Frequently` `Preorder.toLE` `nhds`	—	—	`upperSemicontinuous_iff_frequently`
`of_frequently` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`UpperSemicontinuous`	—	`upperSemicontinuous_iff_frequently`
`upperSemicontinuousAt` 📖	mathematical	`UpperSemicontinuous`	`UpperSemicontinuousAt`	—	—
`upperSemicontinuousOn` 📖	mathematical	`UpperSemicontinuous`	`UpperSemicontinuousOn`	—	`Semicontinuous.semicontinuousOn`
`upperSemicontinuousWithinAt` 📖	mathematical	`UpperSemicontinuous`	`UpperSemicontinuousWithinAt`	—	`SemicontinuousAt.semicontinuousWithinAt`

UpperSemicontinuousAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	—	`UpperSemicontinuousAt` `ContinuousAt`	—	—	`SemicontinuousAt.comp`
`frequently` 📖	—	`UpperSemicontinuousAt` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Filter.Frequently` `Preorder.toLE` `nhds`	—	—	`upperSemicontinuousAt_iff_frequently`
`of_frequently` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`UpperSemicontinuousAt`	—	`upperSemicontinuousAt_iff_frequently`
`upperSemicontinuousWithinAt` 📖	mathematical	`UpperSemicontinuousAt`	`UpperSemicontinuousWithinAt`	—	`SemicontinuousAt.semicontinuousWithinAt`

UpperSemicontinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	—	`UpperSemicontinuousOn` `ContinuousOn` `Set.MapsTo`	—	—	`SemicontinuousOn.comp`
`frequently` 📖	—	`UpperSemicontinuousOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set` `Set.instMembership` `Filter.Frequently` `Preorder.toLE` `nhdsWithin`	—	—	`upperSemicontinuousOn_iff_frequently`
`mono` 📖	—	`UpperSemicontinuousOn` `Set` `Set.instHasSubset`	—	—	`SemicontinuousOn.mono`
`of_frequently` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`UpperSemicontinuousOn`	—	`upperSemicontinuousOn_iff_frequently`
`upperSemicontinuousWithinAt` 📖	mathematical	`UpperSemicontinuousOn` `Set` `Set.instMembership`	`UpperSemicontinuousWithinAt`	—	—

UpperSemicontinuousWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	—	`UpperSemicontinuousWithinAt` `ContinuousWithinAt` `Set.MapsTo`	—	—	`SemicontinuousWithinAt.comp`
`congr_of_eventuallyEq` 📖	—	`UpperSemicontinuousWithinAt` `Set` `Set.instMembership` `Filter.Eventually` `nhdsWithin`	—	—	`LowerSemicontinuousWithinAt.congr_of_eventuallyEq`
`frequently` 📖	—	`UpperSemicontinuousWithinAt` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Filter.Frequently` `Preorder.toLE` `nhdsWithin`	—	—	`upperSemicontinuousWithinAt_iff_frequently`
`mono` 📖	—	`UpperSemicontinuousWithinAt` `Set` `Set.instHasSubset`	—	—	`SemicontinuousWithinAt.mono`
`of_frequently` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`UpperSemicontinuousWithinAt`	—	`upperSemicontinuousWithinAt_iff_frequently`

(root)

Definitions

Name	Category	Theorems
`LowerHemicontinuous` 📖	MathDef	9 math math: `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_iff_frequently`
`LowerHemicontinuousAt` 📖	MathDef	7 math math: `LowerHemicontinuousAt.const`, `lowerHemicontinuous_iff`, `LowerHemicontinuousAt.of_frequently`, `lowerHemicontinuousAt_iff`, `lowerHemicontinuousAt_iff_frequently`, `LowerHemicontinuous.lowerHemicontinuousAt`, `lowerHemicontinuousWithinAt_univ_iff`
`LowerHemicontinuousOn` 📖	MathDef	7 math math: `LowerHemicontinuousOn.const`, `LowerHemicontinuous.lowerHemicontinuousOn`, `LowerHemicontinuousOn.of_frequently`, `lowerHemicontinuous_restrict_iff`, `lowerHemicontinuousOn_iff_frequently`, `lowerHemicontinuousOn_univ_iff`, `lowerHemicontinuousOn_iff`
`LowerHemicontinuousWithinAt` 📖	MathDef	9 math math: `lowerHemicontinuousWithinAt_iff_frequently`, `LowerHemicontinuousOn.lowerHemicontinuousWithinAt`, `LowerHemicontinuousWithinAt.const`, `LowerHemicontinuous.lowerHemicontinuousWithinAt`, `LowerHemicontinuousAt.lowerHemicontinuousWithinAt`, `LowerHemicontinuousWithinAt.of_frequently`, `lowerHemicontinuousWithinAt_univ_iff`, `lowerHemicontinuousOn_iff`, `lowerHemicontinuousWithinAt_iff`
`LowerSemicontinuous` 📖	MathDef	24 math math: `MeasureTheory.exists_lt_lowerSemicontinuous_integral_gt_nnreal`, `lowerSemicontinuous_iff_isClosed_preimage`, `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_iff_isClosed_epigraph`, `MeasureTheory.exists_lt_lowerSemicontinuous_integral_lt`, `MeasureTheory.SimpleFunc.exists_le_lowerSemicontinuous_lintegral_ge`, `lowerSemicontinuous_restrict_iff`, `eVariationOn.lowerSemicontinuous_uniformOn`, `lowerSemicontinuous_const`, `EReal.lowerSemicontinuous_add`, `lowerSemicontinuous_iff`, `Continuous.lowerSemicontinuous`, `lowerSemicontinuousOn_univ_iff`, `Continuous.comp_upperSemicontinuous_antitone`, `lowerSemicontinuous_iff_isOpen_preimage`, `LowerSemicontinuous.of_frequently`, `eVariationOn.lowerSemicontinuous`
`LowerSemicontinuousAt` 📖	MathDef	13 math math: `LowerSemicontinuousAt.of_frequently`, `lowerSemicontinuousAt_const`, `IsClosed.lowerSemicontinuousAt_indicator`, `lowerSemicontinuousWithinAt_univ_iff`, `ContinuousAt.comp_upperSemicontinuousAt_antitone`, `lowerSemicontinuousAt_iff_le_liminf`, `lowerSemicontinuousAt_iff_frequently`, `lowerSemicontinuous_iff`, `LowerSemicontinuous.lowerSemicontinuousAt`, `ContinuousAt.lowerSemicontinuousAt`, `lowerSemicontinuousAt_iff`, `continuousAt_iff_lower_upperSemicontinuousAt`, `IsOpen.lowerSemicontinuousAt_indicator`
`LowerSemicontinuousOn` 📖	MathDef	16 math math: `lowerSemicontinuousOn_const`, `lowerSemicontinuousOn_iff_preimage_Ioi`, `IsOpen.lowerSemicontinuousOn_indicator`, `lowerSemicontinuousOn_iff_isClosed_epigraph`, `continuousOn_iff_lower_upperSemicontinuousOn`, `LowerSemicontinuousOn.of_frequently`, `LowerSemicontinuous.lowerSemicontinuousOn`, `lowerSemicontinuousOn_iff_frequently`, `Continuous.comp_upperSemicontinuousOn_antitone`, `lowerSemicontinuous_restrict_iff`, `ContinuousOn.lowerSemicontinuousOn`, `lowerSemicontinuousOn_iff_preimage_Iic`, `lowerSemicontinuousOn_univ_iff`, `lowerSemicontinuousOn_iff`, `IsClosed.lowerSemicontinuousOn_indicator`, `lowerSemicontinuousOn_iff_le_liminf`
`LowerSemicontinuousWithinAt` 📖	MathDef	15 math math: `LowerSemicontinuousWithinAt.of_frequently`, `continuousWithinAt_iff_lower_upperSemicontinuousWithinAt`, `lowerSemicontinuousWithinAt_univ_iff`, `LowerSemicontinuous.lowerSemicontinuousWithinAt`, `IsOpen.lowerSemicontinuousWithinAt_indicator`, `ContinuousWithinAt.lowerSemicontinuousWithinAt`, `LowerSemicontinuousOn.lowerSemicontinuousWithinAt`, `lowerSemicontinuousWithinAt_iff`, `lowerSemicontinuousWithinAt_iff_le_liminf`, `ContinuousAt.comp_upperSemicontinuousWithinAt_antitone`, `lowerSemicontinuousWithinAt_const`, `LowerSemicontinuousAt.lowerSemicontinuousWithinAt`, `IsClosed.lowerSemicontinuousWithinAt_indicator`, `lowerSemicontinuousOn_iff`, `lowerSemicontinuousWithinAt_iff_frequently`
`SemicontinuousAt` 📖	MathDef	4 math math: `semicontinuousWithinAt_univ_iff`, `Semicontinuous.semicontinuousAt`, `SemicontinuousAt.const`, `semicontinuousAt_iff_frequently`
`SemicontinuousOn` 📖	MathDef	5 math math: `semicontinuousOn_univ_iff`, `semicontinuous_restrict_iff`, `SemicontinuousOn.const`, `Semicontinuous.semicontinuousOn`, `semicontinuousOn_iff_frequently`
`SemicontinuousWithinAt` 📖	MathDef	6 math math: `semicontinuousWithinAt_univ_iff`, `Semicontinuous.semicontinuousWithinAt`, `semicontinuousWithinAt_iff_frequently`, `SemicontinuousWithinAt.const`, `SemicontinuousAt.semicontinuousWithinAt`, `SemicontinuousOn.semicontinuousWithinAt`
`UpperHemicontinuous` 📖	MathDef	18 math math: `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_spectrum_nnreal`, `upperHemicontinuous_quasispectrum_nnreal`, `upperHemicontinuous_singleton_iff`, `upperHemicontinuous_iff`, `upperHemicontinuous_iff_isClosed_compl_preimage_Iic_compl`, `upperHemicontinuousOn_iff_restrict`, `UpperHemicontinuous.const`, `upperHemicontinuous_spectrum`, `isClosedMap_iff_upperHemicontinuous`, `upperHemicontinuous_iff_forall_isOpen`
`UpperHemicontinuousAt` 📖	MathDef	12 math math: `upperHemicontinuousAt_iff_forall_isOpen`, `upperHemicontinuousAt_singleton_iff`, `upperHemicontinuousAt_iff_preimage_Iic`, `UpperHemicontinuousAt.const`, `UpperHemicontinuousAt.of_sequences`, `upperHemicontinuousAt_iff`, `UpperHemicontinuousAt.of_forall_isOpen`, `upperHemicontinuous_iff`, `UpperHemicontinuousAt.of_frequently`, `UpperHemicontinuous.upperHemicontinuousAt`, `upperHemicontinuousWithinAt_univ_iff`, `upperHemicontinuousAt_iff_frequently`
`UpperHemicontinuousOn` 📖	MathDef	11 math math: `UpperHemicontinuousOn.of_frequently`, `UpperHemicontinuousOn.of_forall_isOpen`, `UpperHemicontinuous.upperHemicontinuousOn`, `upperHemicontinuousOn_iff_frequently`, `UpperHemicontinuousOn.const`, `upperHemicontinuousOn_iff_preimage_Iic`, `upperHemicontinuousOn_univ_iff`, `upperHemicontinuousOn_iff_forall_isOpen`, `upperHemicontinuousOn_singleton_iff`, `upperHemicontinuousOn_iff`, `upperHemicontinuousOn_iff_restrict`
`UpperHemicontinuousWithinAt` 📖	MathDef	13 math math: `upperHemicontinuousWithinAt_iff_frequently`, `upperHemicontinuousWithinAt_iff_forall_isOpen`, `UpperHemicontinuousAt.upperHemicontinuousWithinAt`, `upperHemicontinuousWithinAt_iff_preimage_Iic`, `UpperHemicontinuous.upperHemicontinuousWithinAt`, `UpperHemicontinuousWithinAt.of_frequently`, `upperHemicontinuousWithinAt_iff`, `UpperHemicontinuousOn.upperHemicontinuousWithinAt`, `UpperHemicontinuousWithinAt.const`, `upperHemicontinuousOn_iff`, `upperHemicontinuousWithinAt_singleton_iff`, `upperHemicontinuousWithinAt_univ_iff`, `UpperHemicontinuousWithinAt.of_forall_isOpen`
`UpperSemicontinuous` 📖	MathDef	19 math math: `Continuous.upperSemicontinuous`, `MeasureTheory.exists_upperSemicontinuous_le_lintegral_le`, `continuous_iff_lower_upperSemicontinuous`, `upperSemicontinuous_iff`, `UpperSemicontinuous.of_frequently`, `upperSemicontinuous_iff_frequently`, `IsClosed.upperSemicontinuous_indicator`, `upperSemicontinuous_const`, `Continuous.comp_lowerSemicontinuous_antitone`, `upperSemicontinuous_iff_limsup_le`, `upperSemicontinuous_iff_isClosed_preimage`, `upperSemicontinuous_iff_IsClosed_hypograph`, `upperSemicontinuous_iff_isOpen_preimage`, `MeasureTheory.SimpleFunc.exists_upperSemicontinuous_le_lintegral_le`, `IsOpen.upperSemicontinuous_indicator`, `MeasureTheory.exists_upperSemicontinuous_le_integral_le`, `MeasureTheory.exists_upperSemicontinuous_lt_integral_gt`, `upperSemicontinuousOn_iff_restrict`, `upperSemicontinuousOn_univ_iff`
`UpperSemicontinuousAt` 📖	MathDef	13 math math: `upperSemicontinuousAt_iff_frequently`, `ContinuousAt.comp_lowerSemicontinuousAt_antitone`, `upperSemicontinuous_iff`, `upperSemicontinuousAt_iff_limsup_le`, `upperSemicontinuousAt_iff`, `upperSemicontinuousWithinAt_univ_iff`, `IsClosed.upperSemicontinuousAt_indicator`, `IsOpen.upperSemicontinuousAt_indicator`, `UpperSemicontinuousAt.of_frequently`, `UpperSemicontinuous.upperSemicontinuousAt`, `upperSemicontinuousAt_const`, `ContinuousAt.upperSemicontinuousAt`, `continuousAt_iff_lower_upperSemicontinuousAt`
`UpperSemicontinuousOn` 📖	MathDef	16 math math: `Continuous.comp_lowerSemicontinuousOn_antitone`, `upperSemicontinuousOn_iff_limsup_le`, `upperSemicontinuousOn_iff_preimage_Iio`, `ContinuousOn.upperSemicontinuousOn`, `continuousOn_iff_lower_upperSemicontinuousOn`, `upperSemicontinuousOn_const`, `upperSemicontinuousOn_iff_frequently`, `UpperSemicontinuousOn.of_frequently`, `IsOpen.upperSemicontinuousOn_indicator`, `UpperSemicontinuous.upperSemicontinuousOn`, `upperSemicontinuousOn_iff_isClosed_hypograph`, `upperSemicontinuousOn_iff_restrict`, `IsClosed.upperSemicontinuousOn_indicator`, `upperSemicontinuousOn_iff_preimage_Ici`, `upperSemicontinuousOn_iff`, `upperSemicontinuousOn_univ_iff`
`UpperSemicontinuousWithinAt` 📖	MathDef	15 math math: `ContinuousAt.comp_lowerSemicontinuousWithinAt_antitone`, `IsClosed.upperSemicontinuousWithinAt_indicator`, `continuousWithinAt_iff_lower_upperSemicontinuousWithinAt`, `UpperSemicontinuousAt.upperSemicontinuousWithinAt`, `UpperSemicontinuous.upperSemicontinuousWithinAt`, `upperSemicontinuousWithinAt_const`, `upperSemicontinuousWithinAt_iff_limsup_le`, `IsOpen.upperSemicontinuousWithinAt_indicator`, `UpperSemicontinuousOn.upperSemicontinuousWithinAt`, `upperSemicontinuousWithinAt_univ_iff`, `upperSemicontinuousWithinAt_iff`, `UpperSemicontinuousWithinAt.of_frequently`, `ContinuousWithinAt.upperSemicontinuousWithinAt`, `upperSemicontinuousWithinAt_iff_frequently`, `upperSemicontinuousOn_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lowerHemicontinuousAt_iff` 📖	mathematical	—	`LowerHemicontinuousAt` `Filter.Eventually` `Set.Nonempty` `Set` `Set.instInter` `nhds`	—	—
`lowerHemicontinuousAt_iff_frequently` 📖	mathematical	—	`LowerHemicontinuousAt` `Set` `Set.instHasSubset`	—	`lowerHemicontinuousWithinAt_univ_iff` `lowerHemicontinuousWithinAt_iff_frequently` `nhdsWithin_univ`
`lowerHemicontinuousOn_iff` 📖	mathematical	—	`LowerHemicontinuousOn` `LowerHemicontinuousWithinAt`	—	—
`lowerHemicontinuousOn_iff_frequently` 📖	mathematical	—	`LowerHemicontinuousOn` `Set` `Set.instHasSubset`	—	—
`lowerHemicontinuousOn_univ_iff` 📖	mathematical	—	`LowerHemicontinuousOn` `Set.univ` `LowerHemicontinuous`	—	`semicontinuousOn_univ_iff`
`lowerHemicontinuousWithinAt_iff` 📖	mathematical	—	`LowerHemicontinuousWithinAt` `Filter.Eventually` `Set.Nonempty` `Set` `Set.instInter` `nhdsWithin`	—	—
`lowerHemicontinuousWithinAt_iff_frequently` 📖	mathematical	—	`LowerHemicontinuousWithinAt` `Set` `Set.instHasSubset`	—	`lowerHemicontinuousWithinAt_iff` `Function.Surjective.forall` `compl_surjective` `not_imp_not`
`lowerHemicontinuousWithinAt_univ_iff` 📖	mathematical	—	`LowerHemicontinuousWithinAt` `Set.univ` `LowerHemicontinuousAt`	—	`semicontinuousWithinAt_univ_iff`
`lowerHemicontinuous_iff` 📖	mathematical	—	`LowerHemicontinuous` `LowerHemicontinuousAt`	—	—
`lowerHemicontinuous_iff_frequently` 📖	mathematical	—	`LowerHemicontinuous` `Set` `Set.instHasSubset`	—	—
`lowerHemicontinuous_restrict_iff` 📖	mathematical	—	`LowerHemicontinuous` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `Set.restrict` `LowerHemicontinuousOn`	—	`semicontinuous_restrict_iff`
`lowerSemicontinuousAt_const` 📖	mathematical	—	`LowerSemicontinuousAt`	—	`SemicontinuousAt.const`
`lowerSemicontinuousAt_iff` 📖	mathematical	—	`LowerSemicontinuousAt` `Filter.Eventually` `Preorder.toLT` `nhds`	—	—
`lowerSemicontinuousAt_iff_frequently` 📖	mathematical	—	`LowerSemicontinuousAt` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLE`	—	—
`lowerSemicontinuousOn_const` 📖	mathematical	—	`LowerSemicontinuousOn`	—	`SemicontinuousOn.const`
`lowerSemicontinuousOn_iff` 📖	mathematical	—	`LowerSemicontinuousOn` `LowerSemicontinuousWithinAt`	—	—
`lowerSemicontinuousOn_iff_frequently` 📖	mathematical	—	`LowerSemicontinuousOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLE`	—	—
`lowerSemicontinuousOn_univ_iff` 📖	mathematical	—	`LowerSemicontinuousOn` `Set.univ` `LowerSemicontinuous`	—	`semicontinuousOn_univ_iff`
`lowerSemicontinuousWithinAt_const` 📖	mathematical	—	`LowerSemicontinuousWithinAt`	—	`SemicontinuousWithinAt.const`
`lowerSemicontinuousWithinAt_iff` 📖	mathematical	—	`LowerSemicontinuousWithinAt` `Filter.Eventually` `Preorder.toLT` `nhdsWithin`	—	—
`lowerSemicontinuousWithinAt_iff_frequently` 📖	mathematical	—	`LowerSemicontinuousWithinAt` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLE`	—	—
`lowerSemicontinuousWithinAt_univ_iff` 📖	mathematical	—	`LowerSemicontinuousWithinAt` `Set.univ` `LowerSemicontinuousAt`	—	`semicontinuousWithinAt_univ_iff`
`lowerSemicontinuous_const` 📖	mathematical	—	`LowerSemicontinuous`	—	`Semicontinuous.const`
`lowerSemicontinuous_iff` 📖	mathematical	—	`LowerSemicontinuous` `LowerSemicontinuousAt`	—	—
`lowerSemicontinuous_iff_frequently` 📖	mathematical	—	`LowerSemicontinuous` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLE`	—	—
`lowerSemicontinuous_restrict_iff` 📖	mathematical	—	`LowerSemicontinuous` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `Set.restrict` `LowerSemicontinuousOn`	—	`semicontinuous_restrict_iff`
`semicontinuousAt_iff_frequently` 📖	mathematical	—	`SemicontinuousAt`	—	—
`semicontinuousOn_iff_frequently` 📖	mathematical	—	`SemicontinuousOn`	—	—
`semicontinuousOn_univ_iff` 📖	mathematical	—	`SemicontinuousOn` `Set.univ` `Semicontinuous`	—	—
`semicontinuousWithinAt_iff_frequently` 📖	mathematical	—	`SemicontinuousWithinAt`	—	—
`semicontinuousWithinAt_univ_iff` 📖	mathematical	—	`SemicontinuousWithinAt` `Set.univ` `SemicontinuousAt`	—	`nhdsWithin_univ`
`semicontinuous_iff_frequently` 📖	mathematical	—	`Semicontinuous`	—	—
`semicontinuous_restrict_iff` 📖	mathematical	—	`Semicontinuous` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `Set.restrict` `SemicontinuousOn`	—	`SemicontinuousOn.eq_1` `Semicontinuous.eq_1` `SetCoe.forall` `nhdsWithin_eq_map_subtype_coe`
`upperHemicontinuousAt_iff` 📖	mathematical	—	`UpperHemicontinuousAt` `Filter.Eventually` `Set` `Filter` `Filter.instMembership` `nhdsSet` `nhds`	—	—
`upperHemicontinuousAt_iff_frequently` 📖	mathematical	—	`UpperHemicontinuousAt` `Set.Nonempty` `Set` `Set.instInter`	—	`upperHemicontinuousWithinAt_univ_iff` `upperHemicontinuousWithinAt_iff_frequently` `nhdsWithin_univ`
`upperHemicontinuousOn_iff` 📖	mathematical	—	`UpperHemicontinuousOn` `UpperHemicontinuousWithinAt`	—	—
`upperHemicontinuousOn_iff_frequently` 📖	mathematical	—	`UpperHemicontinuousOn` `Set.Nonempty` `Set` `Set.instInter`	—	—
`upperHemicontinuousOn_iff_restrict` 📖	mathematical	—	`UpperHemicontinuous` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `Set.restrict` `UpperHemicontinuousOn`	—	`semicontinuous_restrict_iff`
`upperHemicontinuousOn_univ_iff` 📖	mathematical	—	`UpperHemicontinuousOn` `Set.univ` `UpperHemicontinuous`	—	`semicontinuousOn_univ_iff`
`upperHemicontinuousWithinAt_iff` 📖	mathematical	—	`UpperHemicontinuousWithinAt` `Filter.Eventually` `Set` `Filter` `Filter.instMembership` `nhdsSet` `nhdsWithin`	—	—
`upperHemicontinuousWithinAt_iff_frequently` 📖	mathematical	—	`UpperHemicontinuousWithinAt` `Set.Nonempty` `Set` `Set.instInter`	—	`UpperHemicontinuousWithinAt.eq_1` `semicontinuousWithinAt_iff_frequently` `Function.Surjective.forall` `compl_surjective` `interior_compl`
`upperHemicontinuousWithinAt_univ_iff` 📖	mathematical	—	`UpperHemicontinuousWithinAt` `Set.univ` `UpperHemicontinuousAt`	—	`semicontinuousWithinAt_univ_iff`
`upperHemicontinuous_iff` 📖	mathematical	—	`UpperHemicontinuous` `UpperHemicontinuousAt`	—	—
`upperHemicontinuous_iff_frequently` 📖	mathematical	—	`UpperHemicontinuous` `Set.Nonempty` `Set` `Set.instInter`	—	—
`upperSemicontinuousAt_const` 📖	mathematical	—	`UpperSemicontinuousAt`	—	`SemicontinuousAt.const`
`upperSemicontinuousAt_iff` 📖	mathematical	—	`UpperSemicontinuousAt` `Filter.Eventually` `Preorder.toLT` `nhds`	—	—
`upperSemicontinuousAt_iff_frequently` 📖	mathematical	—	`UpperSemicontinuousAt` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLE`	—	—
`upperSemicontinuousOn_const` 📖	mathematical	—	`UpperSemicontinuousOn`	—	`SemicontinuousOn.const`
`upperSemicontinuousOn_iff` 📖	mathematical	—	`UpperSemicontinuousOn` `UpperSemicontinuousWithinAt`	—	—
`upperSemicontinuousOn_iff_frequently` 📖	mathematical	—	`UpperSemicontinuousOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLE`	—	—
`upperSemicontinuousOn_iff_restrict` 📖	mathematical	—	`UpperSemicontinuous` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `Set.restrict` `UpperSemicontinuousOn`	—	`lowerSemicontinuous_restrict_iff`
`upperSemicontinuousOn_univ_iff` 📖	mathematical	—	`UpperSemicontinuousOn` `Set.univ` `UpperSemicontinuous`	—	`semicontinuousOn_univ_iff`
`upperSemicontinuousWithinAt_const` 📖	mathematical	—	`UpperSemicontinuousWithinAt`	—	`SemicontinuousWithinAt.const`
`upperSemicontinuousWithinAt_iff` 📖	mathematical	—	`UpperSemicontinuousWithinAt` `Filter.Eventually` `Preorder.toLT` `nhdsWithin`	—	—
`upperSemicontinuousWithinAt_iff_frequently` 📖	mathematical	—	`UpperSemicontinuousWithinAt` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLE`	—	—
`upperSemicontinuousWithinAt_univ_iff` 📖	mathematical	—	`UpperSemicontinuousWithinAt` `Set.univ` `UpperSemicontinuousAt`	—	`semicontinuousWithinAt_univ_iff`
`upperSemicontinuous_const` 📖	mathematical	—	`UpperSemicontinuous`	—	`Semicontinuous.const`
`upperSemicontinuous_iff` 📖	mathematical	—	`UpperSemicontinuous` `UpperSemicontinuousAt`	—	—
`upperSemicontinuous_iff_frequently` 📖	mathematical	—	`UpperSemicontinuous` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLE`	—	—

---

← Back to Index