Is Stable right Continuous

lemma isStable_rightContinuous :    IsStable 𝓕 (fun (X : ι → Ω → E) ↦ ∀ ω, Function.IsRightContinuous (X · ω)) := by  refine isStable_pathwise (fun X i ↦ ContinuousWithinAt X (Set.Ioi i) i) (fun _ ↦ by fun_prop)    ?_ ?_  · intro X a hX i hai    specialize hX i    have h_eq : (fun x ↦ X (min x a)) =ᶠ[𝓝[>] i] fun _ ↦ X a := by      rw [eventuallyEq_nhdsWithin_iff]      filter_upwards [] with j hji      rw [min_eq_right]      grind    refine (EventuallyEq.congr_continuousWithinAt h_eq ?_).mpr ?_    · simp [hai]    · fun_prop  · intro X Y i hXY    refine EventuallyEq.congr_continuousWithinAt ?_ ?_    · rw [eventuallyEq_nhdsWithin_iff]      obtain ⟨k, hik, hk⟩ := hXY      filter_upwards [eventually_lt_nhds hik] with j hjk _      exact hk j hjk    · obtain ⟨k, hik, hk⟩ := hXY      exact hk i hik