Compact

📁 Source: Mathlib/Topology/Order/Compact.lean

Statistics

Metric	Count
Definitions `CompactIccSpace`	1
Theorems `isCompact_Icc`, `mk'`, `mk''`, `toCompactIccSpace`, `bddAbove_range_of_hasCompactMulSupport`, `bddAbove_range_of_hasCompactSupport`, `bddBelow_range_of_hasCompactMulSupport`, `bddBelow_range_of_hasCompactSupport`, `exists_forall_ge`, `exists_forall_ge'`, `exists_forall_ge_of_hasCompactMulSupport`, `exists_forall_ge_of_hasCompactSupport`, `exists_forall_le`, `exists_forall_le'`, `exists_forall_le_of_hasCompactMulSupport`, `exists_forall_le_of_hasCompactSupport`, `exists_isMaxOn'`, `exists_isMinOn'`, `image_Icc`, `image_Icc_of_antitoneOn`, `image_Icc_of_monotoneOn`, `image_uIcc`, `image_uIcc_eq_Icc`, `le_sSup_image_Icc`, `sInf_image_Icc_le`, `bddAbove`, `bddAbove_image`, `bddBelow`, `bddBelow_image`, `continuous_sInf`, `continuous_sSup`, `exists_forall_le'`, `exists_isGLB`, `exists_isGreatest`, `exists_isLUB`, `exists_isLeast`, `exists_isLocalMax_mem_open`, `exists_isLocalMin_mem_open`, `exists_isMaxOn`, `exists_isMaxOn_mem_subset`, `exists_isMinOn`, `exists_isMinOn_mem_subset`, `exists_sInf_image_eq`, `exists_sInf_image_eq_and_le`, `exists_sSup_image_eq`, `exists_sSup_image_eq_and_ge`, `isGLB_sInf`, `isGreatest_sSup`, `isLUB_sSup`, `isLeast_sInf`, `lt_sInf_iff_of_continuous`, `sInf_mem`, `sSup_lt_iff_of_continuous`, `sSup_mem`, `compact_Icc_space'`, `atBot_atTop_le_cocompact`, `atBot_le_cocompact`, `atTop_le_cocompact`, `cocompact_eq_atBot`, `cocompact_eq_atBot_atTop`, `cocompact_eq_atTop`, `cocompact_le_atBot`, `cocompact_le_atBot_atTop`, `cocompact_le_atTop`, `compactSpace_Icc`, `compactSpace_of_completeLinearOrder`, `eq_Icc_of_connected_compact`, `instCompactIccSpaceForall`, `instCompactIccSpaceOrderDual`, `instCompactIccSpaceProd`, `isCompact_Ico_iff`, `isCompact_Ioc_iff`, `isCompact_Ioo_iff`, `isCompact_uIcc`	74
Total	75

CompactIccSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCompact_Icc` 📖	mathematical	—	`IsCompact` `Set.Icc`	—	—
`mk'` 📖	mathematical	`IsCompact` `Set.Icc`	`CompactIccSpace`	—	`by_cases` `Set.Icc_eq_empty` `isCompact_empty`
`mk''` 📖	mathematical	`IsCompact` `Set.Icc` `PartialOrder.toPreorder`	`CompactIccSpace`	—	`mk'` `LE.le.eq_or_lt` `Set.Icc_self`

ConditionallyCompleteLinearOrder

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toCompactIccSpace` 📖	mathematical	—	`CompactIccSpace` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `toConditionallyCompleteLattice`	—	`isCompact_Icc`

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bddAbove_range_of_hasCompactMulSupport` 📖	mathematical	`Continuous` `HasCompactMulSupport`	`BddAbove` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.range`	—	`bddBelow_range_of_hasCompactMulSupport` `instClosedIicTopologyOrderDual`
`bddAbove_range_of_hasCompactSupport` 📖	mathematical	`Continuous` `HasCompactSupport`	`BddAbove` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.range`	—	`bddBelow_range_of_hasCompactSupport` `instClosedIicTopologyOrderDual`
`bddBelow_range_of_hasCompactMulSupport` 📖	mathematical	`Continuous` `HasCompactMulSupport`	`BddBelow` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.range`	—	`IsCompact.bddBelow` `One.instNonempty` `HasCompactMulSupport.isCompact_range`
`bddBelow_range_of_hasCompactSupport` 📖	mathematical	`Continuous` `HasCompactSupport`	`BddBelow` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.range`	—	`IsCompact.bddBelow` `Zero.instNonempty` `HasCompactSupport.isCompact_range`
`exists_forall_ge` 📖	mathematical	`Continuous` `Filter.Tendsto` `Filter.cocompact` `Filter.atBot` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Preorder.toLE`	—	`exists_forall_le` `instClosedIicTopologyOrderDual`
`exists_forall_ge'` 📖	—	`Continuous` `Filter.Eventually` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Filter.cocompact`	—	—	`exists_forall_le'` `instClosedIicTopologyOrderDual`
`exists_forall_ge_of_hasCompactMulSupport` 📖	mathematical	`Continuous` `HasCompactMulSupport`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`exists_forall_le_of_hasCompactMulSupport` `instClosedIicTopologyOrderDual`
`exists_forall_ge_of_hasCompactSupport` 📖	mathematical	`Continuous` `HasCompactSupport`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`exists_forall_le_of_hasCompactSupport` `instClosedIicTopologyOrderDual`
`exists_forall_le` 📖	mathematical	`Continuous` `Filter.Tendsto` `Filter.cocompact` `Filter.atTop` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Preorder.toLE`	—	`exists_forall_le'` `Filter.Tendsto.eventually` `Filter.eventually_ge_atTop`
`exists_forall_le'` 📖	—	`Continuous` `Filter.Eventually` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Filter.cocompact`	—	—	`ContinuousOn.exists_isMinOn'` `continuousOn` `isClosed_univ` `Set.mem_univ` `Filter.principal_univ` `inf_top_eq`
`exists_forall_le_of_hasCompactMulSupport` 📖	mathematical	`Continuous` `HasCompactMulSupport`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`IsCompact.exists_isLeast` `HasCompactMulSupport.isCompact_range` `Set.range_nonempty` `Set.forall_mem_range` `mem_lowerBounds`
`exists_forall_le_of_hasCompactSupport` 📖	mathematical	`Continuous` `HasCompactSupport`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`IsCompact.exists_isLeast` `HasCompactSupport.isCompact_range` `Set.range_nonempty` `Set.forall_mem_range` `mem_lowerBounds`

ContinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_isMaxOn'` 📖	mathematical	`ContinuousOn` `Set` `Set.instMembership` `Filter.Eventually` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Filter` `Filter.instInf` `Filter.cocompact` `Filter.principal`	`IsMaxOn`	—	`exists_isMinOn'` `instClosedIicTopologyOrderDual`
`exists_isMinOn'` 📖	mathematical	`ContinuousOn` `Set` `Set.instMembership` `Filter.Eventually` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Filter` `Filter.instInf` `Filter.cocompact` `Filter.principal`	`IsMinOn`	—	`Filter.HasBasis.eventually_iff` `Filter.HasBasis.inf_principal` `Filter.hasBasis_cocompact` `Set.insert_subset_iff` `Set.inter_subset_right` `IsCompact.exists_isMinOn` `IsCompact.insert` `IsCompact.inter_right` `Set.insert_nonempty` `mono` `LE.le.trans`
`image_Icc` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ContinuousOn` `Set.Icc`	`Set.image` `InfSet.sInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet`	—	`eq_Icc_of_connected_compact` `Set.Nonempty.image` `Set.nonempty_Icc` `IsPreconnected.image` `isPreconnected_Icc` `IsCompact.image_of_continuousOn` `CompactIccSpace.isCompact_Icc` `ConditionallyCompleteLinearOrder.toCompactIccSpace`
`image_Icc_of_antitoneOn` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ContinuousOn` `Set.Icc` `AntitoneOn`	`Set.image`	—	`Set.Icc_toDual` `image_Icc_of_monotoneOn` `instOrderTopologyOrderDual` `AntitoneOn.dual_right`
`image_Icc_of_monotoneOn` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ContinuousOn` `Set.Icc` `MonotoneOn`	`Set.image`	—	`image_Icc` `MonotoneOn.sInf_image_Icc` `MonotoneOn.sSup_image_Icc`
`image_uIcc` 📖	mathematical	`ContinuousOn` `Set.uIcc` `ConditionallyCompleteLattice.toLattice` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	`Set.image` `InfSet.sInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup`	—	`image_uIcc_eq_Icc` `Set.uIcc_of_le` `csInf_le_csSup` `bddBelow_Icc` `bddAbove_Icc` `Set.Nonempty.image` `Set.nonempty_uIcc`
`image_uIcc_eq_Icc` 📖	mathematical	`ContinuousOn` `Set.uIcc` `ConditionallyCompleteLattice.toLattice` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	`Set.image` `Set.Icc` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `InfSet.sInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet`	—	`image_Icc` `min_le_max`
`le_sSup_image_Icc` 📖	mathematical	`ContinuousOn` `Set.Icc` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Set` `Set.instMembership`	`Preorder.toLE` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `Set.image`	—	`Set.mem_image_of_mem` `image_Icc` `LE.le.trans`
`sInf_image_Icc_le` 📖	mathematical	`ContinuousOn` `Set.Icc` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Set` `Set.instMembership`	`Preorder.toLE` `InfSet.sInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `Set.image`	—	`Set.mem_image_of_mem` `image_Icc` `LE.le.trans`

IsCompact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bddAbove` 📖	mathematical	`IsCompact`	`BddAbove` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`bddBelow` `instClosedIicTopologyOrderDual` `OrderDual.instNonempty`
`bddAbove_image` 📖	mathematical	`IsCompact` `ContinuousOn`	`BddAbove` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.image`	—	`bddBelow_image` `instClosedIicTopologyOrderDual` `OrderDual.instNonempty`
`bddBelow` 📖	mathematical	`IsCompact`	`BddBelow` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`Set.eq_empty_or_nonempty` `bddBelow_empty` `exists_isLeast`
`bddBelow_image` 📖	mathematical	`IsCompact` `ContinuousOn`	`BddBelow` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.image`	—	`bddBelow` `image_of_continuousOn`
`continuous_sInf` 📖	mathematical	`IsCompact` `Continuous` `instTopologicalSpaceProd` `Function.HasUncurry.uncurry` `Function.hasUncurryInduction` `Function.hasUncurryBase`	`InfSet.sInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Set.image`	—	`continuous_sSup` `instOrderTopologyOrderDual`
`continuous_sSup` 📖	mathematical	`IsCompact` `Continuous` `instTopologicalSpaceProd` `Function.HasUncurry.uncurry` `Function.hasUncurryInduction` `Function.hasUncurryBase`	`SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Set.image`	—	`Set.eq_empty_or_nonempty` `Set.image_empty` `continuous_const` `continuous_iff_continuousAt` `exists_sSup_image_eq_and_ge` `instClosedIciTopology` `OrderTopology.to_orderClosedTopology` `Continuous.continuousOn` `Continuous.comp` `Continuous.prodMk_right` `ContinuousAt.eq_1` `tendsto_order` `Continuous.tendsto` `Continuous.prodMk_left` `Filter.Eventually.mono` `LT.lt.trans_le` `le_csSup` `bddAbove_image` `supSet_to_nonempty` `Set.mem_image_of_mem` `LE.le.trans_lt` `generalized_tube_lemma` `isCompact_singleton` `IsOpen.preimage` `isOpen_Iio` `Filter.eventually_of_mem` `IsOpen.mem_nhds` `Set.singleton_subset_iff` `sSup_lt_iff_of_continuous` `Set.mk_mem_prod`
`exists_forall_le'` 📖	mathematical	`IsCompact` `ContinuousOn` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Preorder.toLE`	—	`Set.eq_empty_or_nonempty` `NoMaxOrder.exists_gt` `exists_isMinOn`
`exists_isGLB` 📖	mathematical	`IsCompact` `Set.Nonempty`	`Set` `Set.instMembership` `IsGLB` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`IsLeast.isGLB` `exists_isLeast`
`exists_isGreatest` 📖	mathematical	`IsCompact` `Set.Nonempty`	`IsGreatest` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`exists_isLeast` `instClosedIicTopologyOrderDual`
`exists_isLUB` 📖	mathematical	`IsCompact` `Set.Nonempty`	`Set` `Set.instMembership` `IsLUB` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`exists_isGLB` `instClosedIicTopologyOrderDual`
`exists_isLeast` 📖	mathematical	`IsCompact` `Set.Nonempty`	`IsLeast` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`Set.biInter_eq_iInter` `elim_directed_family_closed` `Set.Nonempty.to_subtype` `isClosed_Iic` `Set.not_nonempty_iff_eq_empty` `Monotone.directed_ge` `SemilatticeInf.instIsCodirectedOrder` `Set.Iic_subset_Iic` `le_rfl` `Set.mem_iInter₂`
`exists_isLocalMax_mem_open` 📖	mathematical	`IsCompact` `Set` `Set.instHasSubset` `ContinuousOn` `Set.instMembership` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IsOpen`	`IsLocalMax`	—	`exists_isMaxOn_mem_subset` `IsMaxOn.isLocalMax` `mem_nhds_iff`
`exists_isLocalMin_mem_open` 📖	mathematical	`IsCompact` `Set` `Set.instHasSubset` `ContinuousOn` `Set.instMembership` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IsOpen`	`IsLocalMin`	—	`exists_isMinOn_mem_subset` `IsMinOn.isLocalMin` `mem_nhds_iff`
`exists_isMaxOn` 📖	mathematical	`IsCompact` `Set.Nonempty` `ContinuousOn`	`Set` `Set.instMembership` `IsMaxOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`exists_isMinOn` `instClosedIicTopologyOrderDual`
`exists_isMaxOn_mem_subset` 📖	mathematical	`IsCompact` `ContinuousOn` `Set` `Set.instMembership` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`IsMaxOn`	—	`exists_isMaxOn` `by_contra` `LT.lt.not_ge`
`exists_isMinOn` 📖	mathematical	`IsCompact` `Set.Nonempty` `ContinuousOn`	`Set` `Set.instMembership` `IsMinOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`exists_isLeast` `image_of_continuousOn` `Set.Nonempty.image` `Set.forall_mem_image` `Set.mem_image_of_mem` `Set.image_id'`
`exists_isMinOn_mem_subset` 📖	mathematical	`IsCompact` `ContinuousOn` `Set` `Set.instMembership` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`IsMinOn`	—	`exists_isMinOn` `by_contra` `LT.lt.not_ge`
`exists_sInf_image_eq` 📖	mathematical	`IsCompact` `Set.Nonempty` `ContinuousOn`	`Set` `Set.instMembership` `InfSet.sInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Set.image`	—	`exists_sInf_image_eq_and_le`
`exists_sInf_image_eq_and_le` 📖	mathematical	`IsCompact` `Set.Nonempty` `ContinuousOn`	`Set` `Set.instMembership` `InfSet.sInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Set.image` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup`	—	`sInf_mem` `image_of_continuousOn` `Set.Nonempty.image` `Eq.trans_le` `csInf_le` `bddBelow` `supSet_to_nonempty` `Set.mem_image_of_mem`
`exists_sSup_image_eq` 📖	mathematical	`IsCompact` `Set.Nonempty` `ContinuousOn`	`Set` `Set.instMembership` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Set.image`	—	`exists_sInf_image_eq` `instClosedIicTopologyOrderDual`
`exists_sSup_image_eq_and_ge` 📖	mathematical	`IsCompact` `Set.Nonempty` `ContinuousOn`	`Set` `Set.instMembership` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Set.image` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder`	—	`exists_sInf_image_eq_and_le` `instClosedIicTopologyOrderDual`
`isGLB_sInf` 📖	mathematical	`IsCompact` `Set.Nonempty`	`IsGLB` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `InfSet.sInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf`	—	`isGLB_csInf` `bddBelow` `supSet_to_nonempty`
`isGreatest_sSup` 📖	mathematical	`IsCompact` `Set.Nonempty`	`IsGreatest` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet`	—	`isLeast_sInf` `instClosedIicTopologyOrderDual`
`isLUB_sSup` 📖	mathematical	`IsCompact` `Set.Nonempty`	`IsLUB` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet`	—	`isGLB_sInf` `instClosedIicTopologyOrderDual`
`isLeast_sInf` 📖	mathematical	`IsCompact` `Set.Nonempty`	`IsLeast` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `InfSet.sInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf`	—	`sInf_mem` `isGLB_sInf`
`lt_sInf_iff_of_continuous` 📖	mathematical	`IsCompact` `Set.Nonempty` `ContinuousOn`	`Preorder.toLT` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `InfSet.sInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `Set.image`	—	`sSup_lt_iff_of_continuous` `instClosedIciTopologyOrderDual`
`sInf_mem` 📖	mathematical	`IsCompact` `Set.Nonempty`	`Set` `Set.instMembership` `InfSet.sInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`exists_isLeast` `IsLeast.csInf_mem`
`sSup_lt_iff_of_continuous` 📖	mathematical	`IsCompact` `Set.Nonempty` `ContinuousOn`	`Preorder.toLT` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `Set.image`	—	`LE.le.trans_lt` `le_csSup` `bddAbove_image` `supSet_to_nonempty` `Set.mem_image_of_mem` `exists_isMaxOn` `csSup_le` `Set.Nonempty.image`
`sSup_mem` 📖	mathematical	`IsCompact` `Set.Nonempty`	`Set` `Set.instMembership` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`sInf_mem` `instClosedIicTopologyOrderDual`

Pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compact_Icc_space'` 📖	mathematical	—	`CompactIccSpace` `topologicalSpace` `preorder`	—	`instCompactIccSpaceForall`

(root)

Definitions

Name	Category	Theorems
`CompactIccSpace` 📖	CompData	6 math math: `instCompactIccSpaceProd`, `ConditionallyCompleteLinearOrder.toCompactIccSpace`, `instCompactIccSpaceOrderDual`, `CompactIccSpace.mk'`, `Pi.compact_Icc_space'`, `CompactIccSpace.mk''`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`atBot_atTop_le_cocompact` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `Filter.instSup` `Filter.atBot` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Filter.atTop` `Filter.cocompact`	—	`sup_le` `atBot_le_cocompact` `instClosedIicTopology` `atTop_le_cocompact` `instClosedIciTopology`
`atBot_le_cocompact` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `Filter.atBot` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Filter.cocompact`	—	`Filter.mem_cocompact` `Set.eq_empty_or_nonempty` `Set.univ_subset_iff` `Set.compl_univ_iff` `Filter.univ_mem` `IsCompact.exists_isLeast` `NoMinOrder.exists_lt` `Filter.mem_atBot_sets` `SemilatticeInf.instIsCodirectedOrder` `LT.lt.false` `LE.le.trans_lt` `LT.lt.trans_le` `Set.not_notMem`
`atTop_le_cocompact` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `Filter.atTop` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Filter.cocompact`	—	`atBot_le_cocompact` `OrderDual.noMinOrder` `instClosedIicTopologyOrderDual`
`cocompact_eq_atBot` 📖	mathematical	—	`Filter.cocompact` `Filter.atBot` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`LE.le.antisymm` `cocompact_le_atBot` `atBot_le_cocompact`
`cocompact_eq_atBot_atTop` 📖	mathematical	—	`Filter.cocompact` `Filter` `Filter.instSup` `Filter.atBot` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Filter.atTop`	—	`LE.le.antisymm` `cocompact_le_atBot_atTop` `atBot_atTop_le_cocompact`
`cocompact_eq_atTop` 📖	mathematical	—	`Filter.cocompact` `Filter.atTop` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`LE.le.antisymm` `cocompact_le_atTop` `atTop_le_cocompact`
`cocompact_le_atBot` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `Filter.cocompact` `Filter.atBot` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`Filter.mem_cocompact` `isEmpty_or_nonempty` `isCompact_empty` `IsEmpty.false` `Filter.mem_atBot_sets` `SemilatticeInf.instIsCodirectedOrder` `CompactIccSpace.isCompact_Icc` `not_and_or` `le_of_not_ge` `le_top`
`cocompact_le_atBot_atTop` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `Filter.cocompact` `Filter.instSup` `Filter.atBot` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Filter.atTop`	—	`Filter.mem_cocompact` `isEmpty_or_nonempty` `isCompact_empty` `IsEmpty.false` `Filter.mem_atBot_sets` `SemilatticeInf.instIsCodirectedOrder` `Filter.mem_atTop_sets` `SemilatticeSup.instIsDirectedOrder` `CompactIccSpace.isCompact_Icc` `not_and_or` `le_of_not_ge`
`cocompact_le_atTop` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `Filter.cocompact` `Filter.atTop` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`cocompact_le_atBot` `instCompactIccSpaceOrderDual`
`compactSpace_Icc` 📖	mathematical	—	`CompactSpace` `Set.Elem` `Set.Icc` `instTopologicalSpaceSubtype` `Set` `Set.instMembership`	—	`isCompact_iff_compactSpace` `CompactIccSpace.isCompact_Icc`
`compactSpace_of_completeLinearOrder` 📖	mathematical	—	`CompactSpace`	—	`ConditionallyCompleteLinearOrder.toCompactIccSpace`
`eq_Icc_of_connected_compact` 📖	mathematical	`IsConnected` `IsCompact`	`Set.Icc` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `InfSet.sInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet`	—	`eq_Icc_csInf_csSup_of_connected_bdd_closed` `IsCompact.bddBelow` `instClosedIicTopology` `OrderTopology.to_orderClosedTopology` `supSet_to_nonempty` `IsCompact.bddAbove` `instClosedIciTopology` `IsCompact.isClosed` `OrderClosedTopology.to_t2Space`
`instCompactIccSpaceForall` 📖	mathematical	`CompactIccSpace`	`Pi.topologicalSpace` `Pi.preorder`	—	`isCompact_univ_pi` `Set.pi_univ_Icc` `CompactIccSpace.isCompact_Icc`
`instCompactIccSpaceOrderDual` 📖	mathematical	—	`CompactIccSpace` `OrderDual` `OrderDual.instTopologicalSpace` `OrderDual.instPreorder`	—	`Set.Icc_toDual` `CompactIccSpace.isCompact_Icc`
`instCompactIccSpaceProd` 📖	mathematical	—	`CompactIccSpace` `instTopologicalSpaceProd` `Prod.instPreorder`	—	`IsCompact.prod` `CompactIccSpace.isCompact_Icc` `Set.Icc_prod_eq`
`isCompact_Ico_iff` 📖	mathematical	—	`IsCompact` `Set.Ico` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLE`	—	`isClosed_Ico_iff` `IsCompact.isClosed` `OrderClosedTopology.to_t2Space` `OrderTopology.to_orderClosedTopology` `Set.Ico_eq_empty`
`isCompact_Ioc_iff` 📖	mathematical	—	`IsCompact` `Set.Ioc` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLE`	—	`isClosed_Ioc_iff` `IsCompact.isClosed` `OrderClosedTopology.to_t2Space` `OrderTopology.to_orderClosedTopology` `Set.Ioc_eq_empty`
`isCompact_Ioo_iff` 📖	mathematical	—	`IsCompact` `Set.Ioo` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLE`	—	`isClosed_Ioo_iff` `IsCompact.isClosed` `OrderClosedTopology.to_t2Space` `OrderTopology.to_orderClosedTopology` `Set.Ioo_eq_empty`
`isCompact_uIcc` 📖	mathematical	—	`IsCompact` `Set.uIcc` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`CompactIccSpace.isCompact_Icc`

---

← Back to Index