Transitive

📁 Source: Mathlib/Dynamics/Transitive.lean

Statistics

Metric	Count
Definitions IsTopologicallyTransitive, IsTopologicallyTransitive	2
Theorems exists_vadd_inter, isTopologicallyTransitive_iff, isTopologicallyTransitive_iff_dense_iUnion, isTopologicallyTransitive_iff_dense_iUnion_preimage, isTopologicallyTransitive_iff_dense_of_preimage_invariant, isTopologicallyTransitive_of_isMinimal, dense_iUnion_preimage_smul, dense_iUnion_preimage_vadd, dense_iUnion_smul, dense_iUnion_vadd, dense_of_preimage_smul_invariant, dense_of_preimage_vadd_invariant, exists_smul_inter, isTopologicallyTransitive_iff, isTopologicallyTransitive_iff_dense_iUnion, isTopologicallyTransitive_iff_dense_iUnion_preimage, isTopologicallyTransitive_iff_dense_of_preimage_invariant, isTopologicallyTransitive_of_isMinimal	18
Total	20

AddAction

Definitions

Name	Category	Theorems
IsTopologicallyTransitive 📖	CompData	5 math math: isTopologicallyTransitive_iff_dense_iUnion_preimage, isTopologicallyTransitive_iff, isTopologicallyTransitive_iff_dense_iUnion, isTopologicallyTransitive_of_isMinimal, isTopologicallyTransitive_iff_dense_of_preimage_invariant

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isTopologicallyTransitive_iff 📖	mathematical	—	IsTopologicallyTransitive Set.Nonempty Set Set.instInter HVAdd.hVAdd instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup toAddSemigroupAction	—	IsTopologicallyTransitive.exists_vadd_inter
isTopologicallyTransitive_iff_dense_iUnion 📖	mathematical	—	IsTopologicallyTransitive Dense Set.iUnion HVAdd.hVAdd Set instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup toAddSemigroupAction	—	isTopologicallyTransitive_iff Set.inter_comm dense_iff_inter_open Set.inter_iUnion Set.nonempty_iUnion
isTopologicallyTransitive_iff_dense_iUnion_preimage 📖	mathematical	—	IsTopologicallyTransitive Dense Set.iUnion Set.preimage HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup toAddSemigroupAction	—	dense_iff_inter_open Set.inter_iUnion Set.nonempty_iUnion Set.image_inter_nonempty_iff IsTopologicallyTransitive.exists_vadd_inter
isTopologicallyTransitive_iff_dense_of_preimage_invariant 📖	mathematical	—	IsTopologicallyTransitive Dense	—	IsOpen.dense_of_preimage_vadd_invariant isTopologicallyTransitive_iff_dense_iUnion_preimage isOpen_iUnion IsOpen.preimage ContinuousConstVAdd.continuous_const_vadd Set.nonempty_iUnion zero_vadd Set.preimage_iUnion Set.mem_iUnion Set.mem_preimage vadd_vadd
isTopologicallyTransitive_of_isMinimal 📖	mathematical	—	IsTopologicallyTransitive	—	isTopologicallyTransitive_iff_dense_iUnion_preimage IsOpen.iUnion_preimage_vadd dense_univ

AddAction.IsTopologicallyTransitive

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_vadd_inter 📖	mathematical	IsOpen Set.Nonempty	Set Set.instInter HVAdd.hVAdd instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup AddAction.toAddSemigroupAction	—	—

IsOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dense_iUnion_preimage_smul 📖	mathematical	IsOpen Set.Nonempty	Dense Set.iUnion Set.preimage SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction	—	MulAction.isTopologicallyTransitive_iff_dense_iUnion_preimage
dense_iUnion_preimage_vadd 📖	mathematical	IsOpen Set.Nonempty	Dense Set.iUnion Set.preimage HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup AddAction.toAddSemigroupAction	—	AddAction.isTopologicallyTransitive_iff_dense_iUnion_preimage
dense_iUnion_smul 📖	mathematical	IsOpen Set.Nonempty	Dense Set.iUnion Set Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction	—	MulAction.isTopologicallyTransitive_iff_dense_iUnion
dense_iUnion_vadd 📖	mathematical	IsOpen Set.Nonempty	Dense Set.iUnion HVAdd.hVAdd Set instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup AddAction.toAddSemigroupAction	—	AddAction.isTopologicallyTransitive_iff_dense_iUnion
dense_of_preimage_smul_invariant 📖	mathematical	IsOpen Set.Nonempty Set Set.instHasSubset Set.preimage SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction	Dense	—	Dense.mono dense_iUnion_preimage_smul
dense_of_preimage_vadd_invariant 📖	mathematical	IsOpen Set.Nonempty Set Set.instHasSubset Set.preimage HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup AddAction.toAddSemigroupAction	Dense	—	Dense.mono Set.iUnion_subset_iff dense_iUnion_preimage_vadd

MulAction

Definitions

Name	Category	Theorems
IsTopologicallyTransitive 📖	CompData	5 math math: isTopologicallyTransitive_iff_dense_iUnion_preimage, isTopologicallyTransitive_of_isMinimal, isTopologicallyTransitive_iff_dense_iUnion, isTopologicallyTransitive_iff_dense_of_preimage_invariant, isTopologicallyTransitive_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isTopologicallyTransitive_iff 📖	mathematical	—	IsTopologicallyTransitive Set.Nonempty Set Set.instInter Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup toSemigroupAction	—	IsTopologicallyTransitive.exists_smul_inter
isTopologicallyTransitive_iff_dense_iUnion 📖	mathematical	—	IsTopologicallyTransitive Dense Set.iUnion Set Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup toSemigroupAction	—	Set.inter_comm Set.inter_iUnion
isTopologicallyTransitive_iff_dense_iUnion_preimage 📖	mathematical	—	IsTopologicallyTransitive Dense Set.iUnion Set.preimage SemigroupAction.toSMul Monoid.toSemigroup toSemigroupAction	—	Set.inter_iUnion IsTopologicallyTransitive.exists_smul_inter
isTopologicallyTransitive_iff_dense_of_preimage_invariant 📖	mathematical	—	IsTopologicallyTransitive Dense	—	IsOpen.dense_of_preimage_smul_invariant isTopologicallyTransitive_iff_dense_iUnion_preimage isOpen_iUnion IsOpen.preimage ContinuousConstSMul.continuous_const_smul Set.nonempty_iUnion one_smul Set.preimage_iUnion smul_smul
isTopologicallyTransitive_of_isMinimal 📖	mathematical	—	IsTopologicallyTransitive	—	isTopologicallyTransitive_iff_dense_iUnion_preimage IsOpen.iUnion_preimage_smul

MulAction.IsTopologicallyTransitive

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_smul_inter 📖	mathematical	IsOpen Set.Nonempty	Set Set.instInter Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction	—	—

---

← Back to Index