Flow

📁 Source: Mathlib/Dynamics/Flow.lean

Statistics

Metric	Count
Definitions `Flow`, `IsFactorOf`, `IsSemiconjugacy`, `forwardOrbit`, `fromIter`, `id`, `instCoeFunForallForall`, `instInhabited`, `orbit`, `restrict`, `restrictAddSubmonoid`, `restrictNonneg`, `reverse`, `toAddAction`, `toFun`, `toHomeomorph`, `IsForwardInvariant`, `IsFwInvariant`, `IsInvariant`	19
Theorems `flow`, `self`, `trans`, `comp`, `cont`, `isFactorOf`, `semiconj`, `surj`, `coe_restrict_apply`, `cont'`, `continuous`, `continuous_toFun`, `ext`, `ext_iff`, `forwardOrbit_eq_range_nonneg`, `forwardOrbit_subset_orbit`, `id_apply`, `image_eq_preimage_symm`, `isForwardInvariant_forwardOrbit`, `isInvariant_iff_image_eq`, `isInvariant_orbit`, `isSemiconjugacy_id_iff_eq`, `map_add`, `map_add'`, `map_zero`, `map_zero'`, `map_zero_apply`, `mem_orbit`, `mem_orbit_iff`, `mem_orbit_of_mem_forwardOrbit`, `mem_orbit_of_mem_orbit`, `mem_orbit_self`, `nonempty_orbit`, `orbit_eq_range`, `orbit_restrict`, `restrictAddSubmonoid_apply`, `isInvariant`, `isInvariant`, `isForwardInvariant`, `isFwInvariant`, `isForwardInvariant_iff_isInvariant`, `isFwInvariant_iff_isInvariant`, `isInvariant_iff_image`	43
Total	62

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`flow` 📖	mathematical	`Continuous`	`Continuous` `Flow.toFun`	—	`Flow.continuous`

Flow

Definitions

Name	Category	Theorems
`IsFactorOf` 📖	MathDef	3 math math: `IsFactorOf.trans`, `IsFactorOf.self`, `IsSemiconjugacy.isFactorOf`
`IsSemiconjugacy` 📖	CompData	2 math math: `IsSemiconjugacy.comp`, `isSemiconjugacy_id_iff_eq`
`forwardOrbit` 📖	CompOp	3 math math: `forwardOrbit_eq_range_nonneg`, `forwardOrbit_subset_orbit`, `isForwardInvariant_forwardOrbit`
`fromIter` 📖	CompOp	—
`id` 📖	CompOp	1 math math: `id_apply`
`instCoeFunForallForall` 📖	CompOp	—
`instInhabited` 📖	CompOp	—
`orbit` 📖	CompOp	10 math math: `nonempty_orbit`, `orbit_restrict`, `orbit_eq_range`, `mem_orbit_of_mem_forwardOrbit`, `mem_orbit_self`, `mem_orbit`, `forwardOrbit_subset_orbit`, `isInvariant_orbit`, `mem_orbit_of_mem_orbit`, `mem_orbit_iff`
`restrict` 📖	CompOp	2 math math: `orbit_restrict`, `coe_restrict_apply`
`restrictAddSubmonoid` 📖	CompOp	1 math math: `restrictAddSubmonoid_apply`
`restrictNonneg` 📖	CompOp	—
`reverse` 📖	CompOp	—
`toAddAction` 📖	CompOp	—
`toFun` 📖	CompOp	27 math math: `map_zero'`, `Continuous.flow`, `IsSemiconjugacy.semiconj`, `orbit_eq_range`, `cont'`, `omegaLimit_image_eq`, `continuous`, `ext_iff`, `forwardOrbit_eq_range_nonneg`, `coe_restrict_apply`, `mem_orbit`, `isInvariant_orbit`, `mem_orbit_of_mem_orbit`, `omegaLimit_image_subset`, `map_add`, `isForwardInvariant_forwardOrbit`, `map_zero`, `map_add'`, `mem_orbit_iff`, `id_apply`, `restrictAddSubmonoid_apply`, `image_eq_preimage_symm`, `continuous_toFun`, `omegaLimit_omegaLimit`, `map_zero_apply`, `isInvariant_iff_image_eq`, `isInvariant_omegaLimit`
`toHomeomorph` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_restrict_apply` 📖	mathematical	`IsInvariant` `toFun`	`Set` `Set.instMembership` `toFun` `Set.Elem` `instTopologicalSpaceSubtype` `restrict`	—	—
`cont'` 📖	mathematical	—	`Continuous` `instTopologicalSpaceProd` `toFun`	—	—
`continuous` 📖	mathematical	`Continuous`	`Continuous` `toFun`	—	`Continuous.comp` `cont'` `Continuous.prodMk`
`continuous_toFun` 📖	mathematical	—	`Continuous` `toFun` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `IsTopologicalAddGroup.toContinuousAdd`	—	`IsTopologicalAddGroup.toContinuousAdd` `continuous` `continuous_const` `continuous_id'`
`ext` 📖	—	`toFun`	—	—	—
`ext_iff` 📖	mathematical	—	`toFun`	—	`ext`
`forwardOrbit_eq_range_nonneg` 📖	mathematical	—	`forwardOrbit` `Set.range` `Preorder.toLE` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `toFun`	—	—
`forwardOrbit_subset_orbit` 📖	mathematical	—	`Set` `Set.instHasSubset` `forwardOrbit` `orbit`	—	`AddAction.orbit_addSubmonoid_subset`
`id_apply` 📖	mathematical	—	`toFun` `id`	—	—
`image_eq_preimage_symm` 📖	mathematical	—	`Set.image` `toFun` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `IsTopologicalAddGroup.toContinuousAdd` `Set.preimage` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`IsTopologicalAddGroup.toContinuousAdd` `Equiv.image_eq_preimage_symm`
`isForwardInvariant_forwardOrbit` 📖	mathematical	—	`IsForwardInvariant` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `toFun` `forwardOrbit`	—	`IsInvariant.isForwardInvariant` `AddSubmonoid.continuousAdd` `isInvariant_orbit`
`isInvariant_iff_image_eq` 📖	mathematical	—	`IsInvariant` `toFun` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `IsTopologicalAddGroup.toContinuousAdd` `Set.image`	—	`IsTopologicalAddGroup.toContinuousAdd` `isInvariant_iff_image` `Set.Subset.antisymm` `add_neg_cancel` `map_zero` `subset_refl` `Set.instReflSubset`
`isInvariant_orbit` 📖	mathematical	—	`IsInvariant` `toFun` `orbit`	—	`AddAction.mem_orbit_of_mem_orbit`
`isSemiconjugacy_id_iff_eq` 📖	mathematical	—	`IsSemiconjugacy`	—	`ext` `IsSemiconjugacy.semiconj` `continuous_id` `Function.Semiconj.id_left`
`map_add` 📖	mathematical	—	`toFun` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup`	—	`map_add'`
`map_add'` 📖	mathematical	—	`toFun` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup`	—	—
`map_zero` 📖	mathematical	—	`toFun` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`map_zero'`
`map_zero'` 📖	mathematical	—	`toFun` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	—
`map_zero_apply` 📖	mathematical	—	`toFun` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`map_zero'`
`mem_orbit` 📖	mathematical	—	`Set` `Set.instMembership` `orbit` `toFun`	—	`AddAction.mem_orbit`
`mem_orbit_iff` 📖	mathematical	—	`Set` `Set.instMembership` `orbit` `toFun`	—	—
`mem_orbit_of_mem_forwardOrbit` 📖	mathematical	`Set` `Set.instMembership` `forwardOrbit`	`Set` `Set.instMembership` `orbit`	—	`forwardOrbit_subset_orbit`
`mem_orbit_of_mem_orbit` 📖	mathematical	`Set` `Set.instMembership` `orbit`	`Set` `Set.instMembership` `orbit` `toFun`	—	`AddAction.mem_orbit_of_mem_orbit`
`mem_orbit_self` 📖	mathematical	—	`Set` `Set.instMembership` `orbit`	—	`AddAction.mem_orbit_self`
`nonempty_orbit` 📖	mathematical	—	`Set.Nonempty` `orbit`	—	`AddAction.nonempty_orbit`
`orbit_eq_range` 📖	mathematical	—	`orbit` `Set.range` `toFun`	—	—
`orbit_restrict` 📖	mathematical	`IsInvariant` `toFun`	`orbit` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `restrict` `Set.preimage`	—	`Set.ext`
`restrictAddSubmonoid_apply` 📖	mathematical	—	`toFun` `AddSubmonoid` `AddMonoid.toAddZeroClass` `SetLike.instMembership` `AddSubmonoid.instSetLike` `instTopologicalSpaceSubtype` `AddSubmonoid.toAddMonoid` `AddSubmonoid.continuousAdd` `restrictAddSubmonoid`	—	`AddSubmonoid.continuousAdd`

Flow.IsFactorOf

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`self` 📖	mathematical	—	`Flow.IsFactorOf`	—	`Flow.isSemiconjugacy_id_iff_eq`
`trans` 📖	mathematical	`Flow.IsFactorOf`	`Flow.IsFactorOf`	—	`Flow.IsSemiconjugacy.comp`

Flow.IsSemiconjugacy

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	mathematical	`Flow.IsSemiconjugacy`	`Flow.IsSemiconjugacy`	—	`Continuous.comp` `cont` `surj` `Function.Semiconj.comp_left` `semiconj`
`cont` 📖	mathematical	`Flow.IsSemiconjugacy`	`Continuous`	—	—
`isFactorOf` 📖	mathematical	`Flow.IsSemiconjugacy`	`Flow.IsFactorOf`	—	—
`semiconj` 📖	mathematical	`Flow.IsSemiconjugacy`	`Function.Semiconj` `Flow.toFun`	—	—
`surj` 📖	—	`Flow.IsSemiconjugacy`	—	—	—

IsForwardInvariant

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isInvariant` 📖	mathematical	`IsForwardInvariant` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`IsInvariant`	—	`zero_le`

IsFwInvariant

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isInvariant` 📖	mathematical	`IsForwardInvariant` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`IsInvariant`	—	`IsForwardInvariant.isInvariant`

IsInvariant

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isForwardInvariant` 📖	mathematical	`IsInvariant`	`IsForwardInvariant`	—	—
`isFwInvariant` 📖	mathematical	`IsInvariant`	`IsForwardInvariant`	—	`isForwardInvariant`

(root)

Definitions

Name	Category	Theorems
`Flow` 📖	CompData	—
`IsForwardInvariant` 📖	MathDef	5 math math: `IsInvariant.isForwardInvariant`, `Flow.isForwardInvariant_forwardOrbit`, `isForwardInvariant_iff_isInvariant`, `isFwInvariant_iff_isInvariant`, `IsInvariant.isFwInvariant`
`IsFwInvariant` 📖	MathDef	—
`IsInvariant` 📖	MathDef	8 math math: `Flow.isInvariant_orbit`, `isForwardInvariant_iff_isInvariant`, `isInvariant_iff_image`, `isFwInvariant_iff_isInvariant`, `IsForwardInvariant.isInvariant`, `IsFwInvariant.isInvariant`, `Flow.isInvariant_iff_image_eq`, `Flow.isInvariant_omegaLimit`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isForwardInvariant_iff_isInvariant` 📖	mathematical	—	`IsForwardInvariant` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `IsInvariant`	—	`IsForwardInvariant.isInvariant` `IsInvariant.isForwardInvariant`
`isFwInvariant_iff_isInvariant` 📖	mathematical	—	`IsForwardInvariant` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `IsInvariant`	—	`isForwardInvariant_iff_isInvariant`
`isInvariant_iff_image` 📖	mathematical	—	`IsInvariant` `Set` `Set.instHasSubset` `Set.image`	—	—

---

← Back to Index