Flow

📁 Source: Mathlib/Dynamics/Flow.lean

Statistics

Metric	Count
Definitions Flow, IsFactorOf, IsSemiconjugacy, forwardOrbit, fromIter, instCoeFunForallForall, instInhabited, orbit, restrict, restrictAddSubmonoid, restrictNonneg, reverse, toAddAction, toFun, toHomeomorph, IsForwardInvariant, IsFwInvariant, IsInvariant	18
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, 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	42
Total	60

Continuous

Theorems

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

Flow

Definitions

Name	Category	Theorems
IsFactorOf 📖	MathDef	2 math math: IsFactorOf.self, IsSemiconjugacy.isFactorOf
IsSemiconjugacy 📖	CompData	1 math math: isSemiconjugacy_id_iff_eq
forwardOrbit 📖	CompOp	3 math math: forwardOrbit_eq_range_nonneg, forwardOrbit_subset_orbit, isForwardInvariant_forwardOrbit
fromIter 📖	CompOp	—
instCoeFunForallForall 📖	CompOp	—
instInhabited 📖	CompOp	—
orbit 📖	CompOp	9 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_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	25 math math: map_zero', Continuous.flow, IsSemiconjugacy.semiconj, orbit_eq_range, cont', omegaLimit_image_eq, continuous, ext_iff, forwardOrbit_eq_range_nonneg, mem_orbit, isInvariant_orbit, mem_orbit_of_mem_orbit, omegaLimit_image_subset, map_add, isForwardInvariant_forwardOrbit, map_zero, map_add', mem_orbit_iff, 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 Set.Elem instTopologicalSpaceSubtype restrict	—	—
cont' 📖	mathematical	—	Continuous instTopologicalSpaceProd toFun	—	—
continuous 📖	mathematical	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
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	orbit	—	forwardOrbit_subset_orbit
mem_orbit_of_mem_orbit 📖	mathematical	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 📖	—	Flow.IsFactorOf	—	—	Flow.IsSemiconjugacy.comp

Flow.IsSemiconjugacy

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	—	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