Minimal

📁 Source: Mathlib/Dynamics/Minimal.lean

Statistics

Metric	Count
Definitions IsMinimal, IsMinimal	2
Theorems dense_orbit, dense_orbit, isMinimal_of_pretransitive, exists_finite_cover_smul, exists_finite_cover_vadd, exists_smul_mem, exists_vadd_mem, iUnion_preimage_smul, iUnion_preimage_vadd, iUnion_smul, iUnion_vadd, dense_orbit, dense_orbit, isMinimal_of_pretransitive, denseRange_smul, denseRange_vadd, dense_of_nonempty_smul_invariant, dense_of_nonempty_vadd_invariant, eq_empty_or_univ_of_smul_invariant_closed, eq_empty_or_univ_of_vadd_invariant_closed, isMinimal_iff_isClosed_smul_invariant, isMinimal_iff_isClosed_vadd_invariant	22
Total	24

AddAction

Definitions

Name	Category	Theorems
IsMinimal 📖	CompData	2 math math: isMinimal_iff_isClosed_vadd_invariant, isMinimal_of_pretransitive

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dense_orbit 📖	mathematical	—	Dense orbit AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup toAddSemigroupAction	—	IsMinimal.dense_orbit
isMinimal_of_pretransitive 📖	mathematical	—	IsMinimal	—	Function.Surjective.denseRange surjective_vadd

AddAction.IsMinimal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dense_orbit 📖	mathematical	—	Dense AddAction.orbit AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup AddAction.toAddSemigroupAction	—	—

IsCompact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_finite_cover_smul 📖	mathematical	IsCompact IsOpen Set.Nonempty	Set Set.instHasSubset Set.iUnion Finset Finset.instMembership Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction	—	elim_finite_subcover IsOpen.smul Set.subset_univ IsOpen.iUnion_smul
exists_finite_cover_vadd 📖	mathematical	IsCompact IsOpen Set.Nonempty	Set Set.instHasSubset Set.iUnion Finset Finset.instMembership HVAdd.hVAdd instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction	—	elim_finite_subcover IsOpen.vadd Set.subset_univ IsOpen.iUnion_vadd

IsOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_smul_mem 📖	mathematical	IsOpen Set.Nonempty	Set Set.instMembership SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction	—	DenseRange.exists_mem_open denseRange_smul
exists_vadd_mem 📖	mathematical	IsOpen Set.Nonempty	Set Set.instMembership HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup AddAction.toAddSemigroupAction	—	DenseRange.exists_mem_open denseRange_vadd
iUnion_preimage_smul 📖	mathematical	IsOpen Set.Nonempty	Set.iUnion Set.preimage SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction Set.univ	—	Set.iUnion_eq_univ_iff exists_smul_mem
iUnion_preimage_vadd 📖	mathematical	IsOpen Set.Nonempty	Set.iUnion Set.preimage HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup AddAction.toAddSemigroupAction Set.univ	—	Set.iUnion_eq_univ_iff exists_vadd_mem
iUnion_smul 📖	mathematical	IsOpen Set.Nonempty	Set.iUnion Set Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction Set.univ	—	Set.iUnion_eq_univ_iff exists_smul_mem inv_smul_smul
iUnion_vadd 📖	mathematical	IsOpen Set.Nonempty	Set.iUnion HVAdd.hVAdd Set instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction Set.univ	—	Set.iUnion_eq_univ_iff exists_vadd_mem neg_vadd_vadd

MulAction

Definitions

Name	Category	Theorems
IsMinimal 📖	CompData	2 math math: isMinimal_of_pretransitive, isMinimal_iff_isClosed_smul_invariant

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dense_orbit 📖	mathematical	—	Dense orbit SemigroupAction.toSMul Monoid.toSemigroup toSemigroupAction	—	IsMinimal.dense_orbit
isMinimal_of_pretransitive 📖	mathematical	—	IsMinimal	—	Function.Surjective.denseRange surjective_smul

MulAction.IsMinimal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dense_orbit 📖	mathematical	—	Dense MulAction.orbit SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction	—	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
denseRange_smul 📖	mathematical	—	DenseRange SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction	—	MulAction.dense_orbit
denseRange_vadd 📖	mathematical	—	DenseRange HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup AddAction.toAddSemigroupAction	—	AddAction.dense_orbit
dense_of_nonempty_smul_invariant 📖	mathematical	Set.Nonempty Set Set.instHasSubset Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction	Dense	—	Dense.mono Set.range_subset_iff MulAction.dense_orbit
dense_of_nonempty_vadd_invariant 📖	mathematical	Set.Nonempty Set Set.instHasSubset HVAdd.hVAdd instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup AddAction.toAddSemigroupAction	Dense	—	Dense.mono Set.range_subset_iff AddAction.dense_orbit
eq_empty_or_univ_of_smul_invariant_closed 📖	mathematical	Set Set.instHasSubset Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction	Set.instEmptyCollection Set.univ	—	Dense.closure_eq dense_of_nonempty_smul_invariant IsClosed.closure_eq Set.eq_empty_or_nonempty
eq_empty_or_univ_of_vadd_invariant_closed 📖	mathematical	Set Set.instHasSubset HVAdd.hVAdd instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup AddAction.toAddSemigroupAction	Set.instEmptyCollection Set.univ	—	Dense.closure_eq dense_of_nonempty_vadd_invariant IsClosed.closure_eq Set.eq_empty_or_nonempty
isMinimal_iff_isClosed_smul_invariant 📖	mathematical	—	MulAction.IsMinimal Set Set.instEmptyCollection Set.univ	—	eq_empty_or_univ_of_smul_invariant_closed dense_iff_closure_eq isClosed_closure smul_closure_orbit_subset Set.Nonempty.ne_empty Set.Nonempty.closure MulAction.nonempty_orbit
isMinimal_iff_isClosed_vadd_invariant 📖	mathematical	—	AddAction.IsMinimal Set Set.instEmptyCollection Set.univ	—	eq_empty_or_univ_of_vadd_invariant_closed dense_iff_closure_eq isClosed_closure vadd_closure_orbit_subset Set.Nonempty.ne_empty Set.Nonempty.closure AddAction.nonempty_orbit

---

← Back to Index