OmegaLimit

📁 Source: Mathlib/Dynamics/OmegaLimit.lean

Statistics

Metric	Count
Definitions `instInhabitedElemSetSets`, `omegaLimit`, `termω`, `«termω⁺»`, `«termω⁻»`	5
Theorems `isInvariant_omegaLimit`, `omegaLimit_image_eq`, `omegaLimit_image_subset`, `omegaLimit_omegaLimit`, `eventually_closure_subset_of_isCompact_absorbing_of_isOpen_of_omegaLimit_subset`, `eventually_closure_subset_of_isCompact_absorbing_of_isOpen_of_omegaLimit_subset'`, `eventually_closure_subset_of_isOpen_of_omegaLimit_subset`, `eventually_mapsTo_of_isCompact_absorbing_of_isOpen_of_omegaLimit_subset`, `eventually_mapsTo_of_isOpen_of_omegaLimit_subset`, `isClosed_omegaLimit`, `mapsTo_omegaLimit`, `mapsTo_omegaLimit'`, `mem_omegaLimit_iff_frequently`, `mem_omegaLimit_iff_frequently₂`, `mem_omegaLimit_singleton_iff_map_cluster_point`, `nonempty_omegaLimit`, `nonempty_omegaLimit_of_isCompact_absorbing`, `omegaLimit_def`, `omegaLimit_eq_biInter_inter`, `omegaLimit_eq_iInter`, `omegaLimit_eq_iInter_inter`, `omegaLimit_iInter`, `omegaLimit_iUnion`, `omegaLimit_image_eq`, `omegaLimit_inter`, `omegaLimit_mono_left`, `omegaLimit_mono_right`, `omegaLimit_preimage_subset`, `omegaLimit_subset_closure_fw_image`, `omegaLimit_subset_of_tendsto`, `omegaLimit_union`	31
Total	36

Flow

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isInvariant_omegaLimit` 📖	mathematical	`Filter.Tendsto` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup`	`IsInvariant` `toFun` `omegaLimit`	—	`Set.MapsTo.mono_right` `mapsTo_omegaLimit` `Set.mapsTo_id` `map_add` `Continuous.flow` `continuous_const` `continuous_id` `omegaLimit_subset_of_tendsto`
`omegaLimit_image_eq` 📖	mathematical	`Filter.Tendsto` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	`omegaLimit` `toFun` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `IsTopologicalAddGroup.toContinuousAdd` `Set.image`	—	`IsTopologicalAddGroup.toContinuousAdd` `Set.Subset.antisymm` `omegaLimit_image_subset` `Set.image_image` `Set.image_congr` `neg_add_cancel` `map_zero` `Set.image_id'`
`omegaLimit_image_subset` 📖	mathematical	`Filter.Tendsto` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup`	`Set` `Set.instHasSubset` `omegaLimit` `toFun` `Set.image`	—	`omegaLimit_image_eq` `omegaLimit_subset_of_tendsto`
`omegaLimit_omegaLimit` 📖	mathematical	`Filter.Tendsto` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	`Set` `Set.instHasSubset` `omegaLimit` `toFun` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `IsTopologicalAddGroup.toContinuousAdd`	—	`IsTopologicalAddGroup.toContinuousAdd` `mem_nhds_iff` `IsOpen.mem_nhds` `Set.Nonempty.mono` `Set.inter_subset_inter_left` `isInvariant_iff_image` `isInvariant_omegaLimit` `omegaLimit_subset_closure_fw_image` `mem_closure_iff_nhds`

(root)

Definitions

Name	Category	Theorems
`instInhabitedElemSetSets` 📖	CompOp	—
`omegaLimit` 📖	CompOp	26 math math: `omegaLimit_preimage_subset`, `omegaLimit_union`, `omegaLimit_iUnion`, `omegaLimit_def`, `Flow.omegaLimit_image_eq`, `omegaLimit_mono_right`, `nonempty_omegaLimit_of_isCompact_absorbing`, `omegaLimit_subset_of_tendsto`, `omegaLimit_image_eq`, `Flow.omegaLimit_image_subset`, `mapsTo_omegaLimit`, `omegaLimit_inter`, `omegaLimit_eq_biInter_inter`, `mem_omegaLimit_iff_frequently`, `mapsTo_omegaLimit'`, `nonempty_omegaLimit`, `mem_omegaLimit_iff_frequently₂`, `omegaLimit_mono_left`, `isClosed_omegaLimit`, `Flow.omegaLimit_omegaLimit`, `omegaLimit_iInter`, `omegaLimit_subset_closure_fw_image`, `omegaLimit_eq_iInter`, `omegaLimit_eq_iInter_inter`, `mem_omegaLimit_singleton_iff_map_cluster_point`, `Flow.isInvariant_omegaLimit`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eventually_closure_subset_of_isCompact_absorbing_of_isOpen_of_omegaLimit_subset` 📖	mathematical	`IsCompact` `Filter.Eventually` `Set.MapsTo` `IsOpen` `Set` `Set.instHasSubset` `omegaLimit`	`Filter` `Filter.instMembership` `closure` `Set.image2`	—	`eventually_closure_subset_of_isCompact_absorbing_of_isOpen_of_omegaLimit_subset'` `closure_minimal` `Set.image2_subset_iff` `IsCompact.isClosed`
`eventually_closure_subset_of_isCompact_absorbing_of_isOpen_of_omegaLimit_subset'` 📖	—	`IsCompact` `Set` `Filter` `Filter.instMembership` `Set.instHasSubset` `closure` `Set.image2` `IsOpen` `omegaLimit`	—	—	`IsCompact.diff` `IsCompact.of_isClosed_subset` `isClosed_closure` `isOpen_compl_iff` `Set.biUnion_eq_iUnion` `Set.diff_subset_comm` `Set.diff_iUnion` `Set.diff_compl` `Set.inter_iInter` `Set.Subset.trans` `Set.inter_subset_right` `omegaLimit_eq_iInter_inter` `IsCompact.elim_finite_subcover_image` `Set.iUnion_congr_Prop` `closure_mono` `Set.image2_subset` `Set.inter_subset_inter` `Set.iInter_subset_of_subset` `Set.Subset.rfl` `subset_refl` `Set.instReflSubset` `Set.union_comm` `Set.inter_subset` `Set.diff_eq` `Set.inter_comm` `Set.compl_subset_compl` `Set.union_subset`
`eventually_closure_subset_of_isOpen_of_omegaLimit_subset` 📖	mathematical	`IsOpen` `Set` `Set.instHasSubset` `omegaLimit`	`Filter` `Filter.instMembership` `closure` `Set.image2`	—	`eventually_closure_subset_of_isCompact_absorbing_of_isOpen_of_omegaLimit_subset'` `isCompact_univ` `Filter.univ_mem` `Set.subset_univ`
`eventually_mapsTo_of_isCompact_absorbing_of_isOpen_of_omegaLimit_subset` 📖	—	`IsCompact` `Filter.Eventually` `Set.MapsTo` `IsOpen` `Set` `Set.instHasSubset` `omegaLimit`	—	—	`eventually_closure_subset_of_isCompact_absorbing_of_isOpen_of_omegaLimit_subset` `Filter.mem_of_superset` `subset_closure` `Set.mem_image2_of_mem`
`eventually_mapsTo_of_isOpen_of_omegaLimit_subset` 📖	mathematical	`IsOpen` `Set` `Set.instHasSubset` `omegaLimit`	`Filter.Eventually` `Set.MapsTo`	—	`eventually_closure_subset_of_isOpen_of_omegaLimit_subset` `Filter.mem_of_superset` `subset_closure` `Set.mem_image2_of_mem`
`isClosed_omegaLimit` 📖	mathematical	—	`IsClosed` `omegaLimit`	—	`isClosed_iInter` `isClosed_closure`
`mapsTo_omegaLimit` 📖	mathematical	`Set.MapsTo` `Continuous`	`omegaLimit`	—	`mapsTo_omegaLimit'` `Filter.Eventually.of_forall`
`mapsTo_omegaLimit'` 📖	mathematical	`Set.MapsTo` `Filter.Eventually` `Set.EqOn` `Continuous`	`omegaLimit`	—	`map_mem_closure` `Filter.inter_mem` `Set.forall_mem_image2` `Set.mem_image2_of_mem`
`mem_omegaLimit_iff_frequently` 📖	mathematical	—	`Set` `Set.instMembership` `omegaLimit` `Filter.Frequently` `Set.Nonempty` `Set.instInter` `Set.preimage`	—	`Set.mem_preimage`
`mem_omegaLimit_iff_frequently₂` 📖	mathematical	—	`Set` `Set.instMembership` `omegaLimit` `Filter.Frequently` `Set.Nonempty` `Set.instInter` `Set.image`	—	—
`mem_omegaLimit_singleton_iff_map_cluster_point` 📖	mathematical	—	`Set` `Set.instMembership` `omegaLimit` `Set.instSingletonSet` `MapClusterPt`	—	—
`nonempty_omegaLimit` 📖	mathematical	`Set.Nonempty`	`omegaLimit`	—	`nonempty_omegaLimit_of_isCompact_absorbing` `isCompact_univ` `Filter.univ_mem` `Set.subset_univ`
`nonempty_omegaLimit_of_isCompact_absorbing` 📖	mathematical	`IsCompact` `Set` `Filter` `Filter.instMembership` `Set.instHasSubset` `closure` `Set.image2` `Set.Nonempty`	`omegaLimit`	—	`omegaLimit_eq_iInter_inter` `IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed` `Filter.inter_mem` `closure_mono` `Set.image2_subset` `Set.inter_subset_inter_left` `Set.Subset.rfl` `Set.Nonempty.image2` `Filter.nonempty_of_mem` `Subtype.prop` `Set.Nonempty.mono` `subset_closure` `IsCompact.of_isClosed_subset` `isClosed_closure` `Set.inter_subset_right`
`omegaLimit_def` 📖	mathematical	—	`omegaLimit` `Set.iInter` `Set` `Filter` `Filter.instMembership` `closure` `Set.image2`	—	—
`omegaLimit_eq_biInter_inter` 📖	mathematical	`Set` `Filter` `Filter.instMembership`	`omegaLimit` `Set.iInter` `closure` `Set.image2` `Set.instInter`	—	`Set.Subset.antisymm` `Set.iInter₂_mono'` `Filter.inter_mem` `Set.Subset.rfl` `Set.iInter₂_mono` `closure_mono` `Set.image2_subset` `Set.inter_subset_left`
`omegaLimit_eq_iInter` 📖	mathematical	—	`omegaLimit` `Set.iInter` `Set.Elem` `Set` `Filter.sets` `closure` `Set.image2` `Set.instMembership`	—	`Set.biInter_eq_iInter`
`omegaLimit_eq_iInter_inter` 📖	mathematical	`Set` `Filter` `Filter.instMembership`	`omegaLimit` `Set.iInter` `Set.Elem` `Filter.sets` `closure` `Set.image2` `Set.instInter` `Set.instMembership`	—	`omegaLimit_eq_biInter_inter` `Set.biInter_eq_iInter`
`omegaLimit_iInter` 📖	mathematical	—	`Set` `Set.instHasSubset` `omegaLimit` `Set.iInter`	—	`Set.subset_iInter` `omegaLimit_mono_right` `Set.iInter_subset`
`omegaLimit_iUnion` 📖	mathematical	—	`Set` `Set.instHasSubset` `Set.iUnion` `omegaLimit`	—	`Set.iUnion_subset_iff` `omegaLimit_mono_right` `Set.subset_iUnion`
`omegaLimit_image_eq` 📖	mathematical	—	`omegaLimit` `Set.image`	—	`Set.iInter_congr_Prop` `Set.image2_image_right`
`omegaLimit_inter` 📖	mathematical	—	`Set` `Set.instHasSubset` `omegaLimit` `Set.instInter`	—	`Set.subset_inter` `omegaLimit_mono_right` `Set.inter_subset_left` `Set.inter_subset_right`
`omegaLimit_mono_left` 📖	mathematical	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder`	`Set` `Set.instHasSubset` `omegaLimit`	—	`omegaLimit_subset_of_tendsto` `Filter.tendsto_id'`
`omegaLimit_mono_right` 📖	mathematical	`Set` `Set.instHasSubset`	`omegaLimit`	—	`Set.iInter₂_mono` `closure_mono` `Set.image2_subset` `Set.Subset.rfl`
`omegaLimit_preimage_subset` 📖	mathematical	—	`Set` `Set.instHasSubset` `omegaLimit` `Set.preimage`	—	`mapsTo_omegaLimit` `Set.mapsTo_preimage` `continuous_id`
`omegaLimit_subset_closure_fw_image` 📖	mathematical	`Set` `Filter` `Filter.instMembership`	`Set.instHasSubset` `omegaLimit` `closure` `Set.image2`	—	`omegaLimit_eq_iInter` `Set.mem_iInter`
`omegaLimit_subset_of_tendsto` 📖	mathematical	`Filter.Tendsto`	`Set` `Set.instHasSubset` `omegaLimit`	—	`Set.iInter₂_mono'` `Filter.tendsto_def` `Set.image2_image_left` `closure_mono` `Set.image2_subset` `Set.image_preimage_subset` `Set.Subset.rfl`
`omegaLimit_union` 📖	mathematical	—	`omegaLimit` `Set` `Set.instUnion`	—	`Set.ext` `Set.union_inter_distrib_right` `Mathlib.Tactic.Contrapose.contrapose₁` `Mathlib.Tactic.Push.not_forall_eq` `Filter.inter_mem` `Filter.Eventually.mono` `Set.Subset.trans` `Set.inter_subset_inter_right` `Set.preimage_mono` `Set.inter_subset_left` `Set.inter_subset_right` `omegaLimit_mono_right` `Set.subset_union_left` `Set.subset_union_right`

omegaLimit

Definitions

Name	Category	Theorems
`termω` 📖	CompOp	—
`«termω⁺»` 📖	CompOp	—
`«termω⁻»` 📖	CompOp	—

---

← Back to Index