Commit 2023-02-05 18:39 9ed3b239

View on Github →

feat: port Dynamics.Minimal (#2075)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Dynamics/Minimal.lean

added theorem IsCompact.exists_finite_cover_smul

added theorem IsOpen.exists_smul_mem

added theorem IsOpen.unionᵢ_preimage_smul

added theorem IsOpen.unionᵢ_smul

added theorem MulAction.dense_orbit

added theorem denseRange_smul

added theorem dense_of_nonempty_smul_invariant

added theorem eq_empty_or_univ_of_smul_invariant_closed

added theorem isMinimal_iff_closed_smul_invariant