Subset

📁 Source: Mathlib/Dynamics/TopologicalEntropy/Subset.lean

Statistics

Metric	Count
Definitions `coverEntropy_supBotHom`, `Subset`, `Subset`, `Subset`, `Subset`	5
Theorems `closure`, `monotone_subset`, `union`, `monotone_subset`, `coverEntropyEntourage_closure`, `coverEntropyEntourage_monotone`, `coverEntropyEntourage_union`, `coverEntropyInfEntourage_closure`, `coverEntropyInfEntourage_monotone`, `coverEntropyInf_biUnion_le`, `coverEntropyInf_closure`, `coverEntropyInf_iUnion_le`, `coverEntropyInf_monotone`, `coverEntropy_biUnion_finset`, `coverEntropy_biUnion_le`, `coverEntropy_closure`, `coverEntropy_iUnion_le`, `coverEntropy_iUnion_of_finite`, `coverEntropy_monotone`, `coverEntropy_union`, `coverMincard_closure_le`, `coverMincard_monotone_subset`, `coverMincard_union_le`, `netEntropyEntourage_monotone`, `netEntropyInfEntourage_monotone`, `netMaxcard_monotone_subset`	26
Total	31

Dynamics

Definitions

Name	Category	Theorems
`coverEntropy_supBotHom` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coverEntropyEntourage_closure` 📖	mathematical	`Continuous` `UniformSpace.toTopologicalSpace` `SetRel` `Filter` `Filter.instMembership` `uniformity`	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `coverEntropyEntourage` `closure` `SetRel.comp`	—	`ExpGrowth.expGrowthSup_monotone` `ENat.toENNReal_mono` `coverMincard_closure_le`
`coverEntropyEntourage_monotone` 📖	mathematical	—	`Monotone` `Set` `EReal` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `instPartialOrderEReal` `coverEntropyEntourage`	—	`ExpGrowth.expGrowthSup_monotone` `ENat.toENNReal_mono` `coverMincard_monotone_subset`
`coverEntropyEntourage_union` 📖	mathematical	—	`coverEntropyEntourage` `Set` `Set.instUnion` `EReal` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal`	—	`le_antisymm` `ExpGrowth.expGrowthSup_monotone` `Pi.add_apply` `ENat.toENNReal_add` `ENat.toENNReal_mono` `coverMincard_union_le` `ExpGrowth.expGrowthSup_add` `max_le` `coverEntropyEntourage_monotone` `Set.subset_union_left` `Set.subset_union_right`
`coverEntropyInfEntourage_closure` 📖	mathematical	`Continuous` `UniformSpace.toTopologicalSpace` `SetRel` `Filter` `Filter.instMembership` `uniformity`	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `coverEntropyInfEntourage` `closure` `SetRel.comp`	—	`ExpGrowth.expGrowthInf_monotone` `ENat.toENNReal_mono` `coverMincard_closure_le`
`coverEntropyInfEntourage_monotone` 📖	mathematical	—	`Monotone` `Set` `EReal` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `instPartialOrderEReal` `coverEntropyInfEntourage`	—	`ExpGrowth.expGrowthInf_monotone` `ENat.toENNReal_mono` `coverMincard_monotone_subset`
`coverEntropyInf_biUnion_le` 📖	mathematical	—	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `iSup` `instSupSetEReal` `Set` `Set.instMembership` `coverEntropyInf` `Set.iUnion`	—	`iSup₂_le` `coverEntropyInf_monotone` `Set.subset_biUnion_of_mem`
`coverEntropyInf_closure` 📖	mathematical	`Continuous` `UniformSpace.toTopologicalSpace`	`coverEntropyInf` `closure`	—	`LE.le.antisymm` `iSup₂_le` `comp_mem_uniformity_sets` `le_iSup₂_of_le` `LE.le.trans` `coverEntropyInfEntourage_antitone` `coverEntropyInfEntourage_closure` `coverEntropyInf_monotone` `subset_closure`
`coverEntropyInf_iUnion_le` 📖	mathematical	—	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `iSup` `instSupSetEReal` `coverEntropyInf` `Set.iUnion`	—	`iSup_le` `coverEntropyInf_monotone` `Set.subset_iUnion`
`coverEntropyInf_monotone` 📖	mathematical	—	`Monotone` `Set` `EReal` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `instPartialOrderEReal` `coverEntropyInf`	—	`iSup₂_mono` `coverEntropyInfEntourage_monotone`
`coverEntropy_biUnion_finset` 📖	mathematical	—	`coverEntropy` `Set.iUnion` `Finset` `Finset.instMembership` `iSup` `EReal` `instSupSetEReal`	—	`map_finset_sup` `SupBotHom.instSupBotHomClass` `coverEntropy_union` `coverEntropy_empty` `coverEntropy_supBotHom.eq_1` `Finset.sup_eq_iSup` `Finset.sup_set_eq_biUnion`
`coverEntropy_biUnion_le` 📖	mathematical	—	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `iSup` `instSupSetEReal` `Set` `Set.instMembership` `coverEntropy` `Set.iUnion`	—	`iSup₂_le` `coverEntropy_monotone` `Set.subset_biUnion_of_mem`
`coverEntropy_closure` 📖	mathematical	`Continuous` `UniformSpace.toTopologicalSpace`	`coverEntropy` `closure`	—	`LE.le.antisymm` `iSup₂_le` `comp_mem_uniformity_sets` `le_iSup₂_of_le` `LE.le.trans` `coverEntropyEntourage_antitone` `coverEntropyEntourage_closure` `coverEntropy_monotone` `subset_closure`
`coverEntropy_iUnion_le` 📖	mathematical	—	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `iSup` `instSupSetEReal` `coverEntropy` `Set.iUnion`	—	`iSup_le` `coverEntropy_monotone` `Set.subset_iUnion`
`coverEntropy_iUnion_of_finite` 📖	mathematical	—	`coverEntropy` `Set.iUnion` `iSup` `EReal` `instSupSetEReal`	—	`Set.map_finite_iSup` `SupBotHom.instSupBotHomClass`
`coverEntropy_monotone` 📖	mathematical	—	`Monotone` `Set` `EReal` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `instPartialOrderEReal` `coverEntropy`	—	`iSup₂_mono` `coverEntropyEntourage_monotone`
`coverEntropy_union` 📖	mathematical	—	`coverEntropy` `Set` `Set.instUnion` `EReal` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal`	—	`biSup_congr` `coverEntropyEntourage_union`
`coverMincard_closure_le` 📖	mathematical	`Continuous` `UniformSpace.toTopologicalSpace` `SetRel` `Filter` `Filter.instMembership` `uniformity`	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `coverMincard` `closure` `SetRel.comp`	—	`eq_top_or_lt_top` `le_top` `coverMincard_finite_iff` `IsDynCoverOf.coverMincard_le_card` `IsDynCoverOf.closure`
`coverMincard_monotone_subset` 📖	mathematical	—	`Monotone` `Set` `ENat` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `coverMincard`	—	`biInf_mono` `IsDynCoverOf.monotone_subset`
`coverMincard_union_le` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `coverMincard` `Set` `Set.instUnion` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	`eq_top_or_lt_top` `top_add` `le_top` `add_top` `coverMincard_finite_iff` `ENat.coe_add` `LE.le.trans` `IsDynCoverOf.coverMincard_le_card` `Finset.coe_union` `IsDynCoverOf.union` `WithTop.coe_mono` `Finset.card_union_le`
`netEntropyEntourage_monotone` 📖	mathematical	—	`Monotone` `Set` `EReal` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `instPartialOrderEReal` `netEntropyEntourage`	—	`ExpGrowth.expGrowthSup_monotone` `ENat.toENNReal_mono` `netMaxcard_monotone_subset`
`netEntropyInfEntourage_monotone` 📖	mathematical	—	`Monotone` `Set` `EReal` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `instPartialOrderEReal` `netEntropyInfEntourage`	—	`ExpGrowth.expGrowthInf_monotone` `ENat.toENNReal_mono` `netMaxcard_monotone_subset`
`netMaxcard_monotone_subset` 📖	mathematical	—	`Monotone` `Set` `ENat` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `netMaxcard`	—	`biSup_mono` `IsDynNetIn.monotone_subset`

Dynamics.IsDynCoverOf

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure` 📖	mathematical	`Continuous` `UniformSpace.toTopologicalSpace` `SetRel` `Filter` `Filter.instMembership` `uniformity` `Dynamics.IsDynCoverOf`	`closure` `SetRel.comp`	—	`Filter.HasBasis.mem_iff'` `UniformSpace.hasBasis_symmetric` `of_entourage_subset` `SetRel.comp_subset_comp_left` `mem_closure_iff_nhds` `Dynamics.ball_dynEntourage_mem_nhds` `Dynamics.dynEntourage_comp_subset`
`monotone_subset` 📖	—	`Set` `Set.instHasSubset` `Dynamics.IsDynCoverOf`	—	—	`HasSubset.Subset.trans` `Set.instIsTransSubset`
`union` 📖	mathematical	`Dynamics.IsDynCoverOf`	`Set` `Set.instUnion`	—	`SetRel.IsCover.union`

Dynamics.IsDynNetIn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`monotone_subset` 📖	—	`Set` `Set.instHasSubset` `Dynamics.IsDynNetIn`	—	—	`HasSubset.Subset.trans` `Set.instIsTransSubset`

Lists'

Definitions

Name	Category	Theorems
`Subset` 📖	CompData	—

Multiset

Definitions

Name	Category	Theorems
`Subset` 📖	MathDef	—

PSet

Definitions

Name	Category	Theorems
`Subset` 📖	MathDef	—

ZFSet

Definitions

Name	Category	Theorems
`Subset` 📖	MathDef	—

---

← Back to Index