English
Applying the omega-limit operation twice yields a subset of applying it once: ω f ϕ (ω f ϕ s) ⊆ ω f ϕ s.
Русский
Повторное применение ω‑лимита даёт подмножество по сравнению с первым применением: ω f ϕ (ω f ϕ s) ⊆ ω f ϕ s.
LaTeX
$$$ \omega f ϕ (ω f ϕ s) \subseteq ω f ϕ s. $$$
Lean4
theorem omegaLimit_omegaLimit (hf : ∀ t, Tendsto (t + ·) f f) : ω f ϕ (ω f ϕ s) ⊆ ω f ϕ s :=
by
simp only [subset_def, mem_omegaLimit_iff_frequently₂, frequently_iff]
intro _ h
rintro n hn u hu
rcases mem_nhds_iff.mp hn with ⟨o, ho₁, ho₂, ho₃⟩
rcases h o (IsOpen.mem_nhds ho₂ ho₃) hu with ⟨t, _ht₁, ht₂⟩
have l₁ : (ω f ϕ s ∩ o).Nonempty :=
ht₂.mono (inter_subset_inter_left _ ((isInvariant_iff_image _ _).mp (isInvariant_omegaLimit _ _ _ hf) _))
have l₂ : (closure (image2 ϕ u s) ∩ o).Nonempty :=
l₁.mono fun b hb ↦ ⟨omegaLimit_subset_closure_fw_image _ _ _ hu hb.1, hb.2⟩
have l₃ : (o ∩ image2 ϕ u s).Nonempty := by
rcases l₂ with ⟨b, hb₁, hb₂⟩
exact mem_closure_iff_nhds.mp hb₁ o (IsOpen.mem_nhds ho₂ hb₂)
rcases l₃ with ⟨ϕra, ho, ⟨_, hr, _, ha, hϕra⟩⟩
exact ⟨_, hr, ϕra, ⟨_, ha, hϕra⟩, ho₁ ho⟩
