From 8f2c7a88af3aefcf9f03f80b1010ca18eb80716c Mon Sep 17 00:00:00 2001 From: Sfgangloff Date: Tue, 12 May 2026 23:30:46 +0900 Subject: [PATCH 1/2] Add monotonicity lemma for LanguageOn MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Prove that the language of a set of configurations is monotone with respect to inclusion of configuration sets: X ⊆ Y → LanguageOn X U ⊆ LanguageOn Y U The proof is a direct unfolding of definitions: a pattern in the language of X comes from restricting some configuration x ∈ X, and inclusion X ⊆ Y allows the same witness to be used for Y. --- Mathlib/Dynamics/SymbolicDynamics/Basic.lean | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/Mathlib/Dynamics/SymbolicDynamics/Basic.lean b/Mathlib/Dynamics/SymbolicDynamics/Basic.lean index 7a1b4e3ff47d53..0e2f2c66628e10 100644 --- a/Mathlib/Dynamics/SymbolicDynamics/Basic.lean +++ b/Mathlib/Dynamics/SymbolicDynamics/Basic.lean @@ -579,7 +579,7 @@ end DefSubshiftByForbidden section Language -variable {A : Type*} [Fintype A] [Inhabited A] +variable {A : Type*} [Inhabited A] variable {G : Type*} /-- Patterns with support exactly `U` form a finite set. -/ @@ -616,6 +616,14 @@ This is the set of all finite patterns obtained by restricting some configuratio def LanguageOn (X : Set (G → A)) (U : Finset G) : Set (Pattern A G) := { p | ∃ x ∈ X, Pattern.fromConfig x U = p } +/-- Considering two sets of configurations `X` and `Y` such that `X ⊆ Y`, the language +of `X` on (finite) shape `U` is included in the language of `Y` on shape `U`. -/ +lemma isMonotonous_LanguageOn {X Y : Set (G → A)} (h : X ⊆ Y) (U : Finset G) : + LanguageOn X U ⊆ LanguageOn Y U := by + intro p hp + rcases hp with ⟨x, hxX, rfl⟩ + exact ⟨x, h hxX, rfl⟩ + /-- The language of a subshift `Y` on a finite shape `U`. -/ def MulSubshift.languageOn {A G} [TopologicalSpace A] [Inhabited A] [Monoid G] (Y : MulSubshift A G) (U : Finset G) : Set (Pattern A G) := From 723fd797a81b74e2c0a3ffc65f71ed5ba0861dc7 Mon Sep 17 00:00:00 2001 From: Sfgangloff Date: Tue, 12 May 2026 23:45:04 +0900 Subject: [PATCH 2/2] fix: naming convention isMonotone_LanguageOn --- Mathlib/Dynamics/SymbolicDynamics/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Dynamics/SymbolicDynamics/Basic.lean b/Mathlib/Dynamics/SymbolicDynamics/Basic.lean index 0e2f2c66628e10..b2c2a08c4deaf2 100644 --- a/Mathlib/Dynamics/SymbolicDynamics/Basic.lean +++ b/Mathlib/Dynamics/SymbolicDynamics/Basic.lean @@ -618,7 +618,7 @@ def LanguageOn (X : Set (G → A)) (U : Finset G) : Set (Pattern A G) := /-- Considering two sets of configurations `X` and `Y` such that `X ⊆ Y`, the language of `X` on (finite) shape `U` is included in the language of `Y` on shape `U`. -/ -lemma isMonotonous_LanguageOn {X Y : Set (G → A)} (h : X ⊆ Y) (U : Finset G) : +lemma isMonotone_LanguageOn {X Y : Set (G → A)} (h : X ⊆ Y) (U : Finset G) : LanguageOn X U ⊆ LanguageOn Y U := by intro p hp rcases hp with ⟨x, hxX, rfl⟩