import PhysicsLogic.Paradigm.OrderedLimits

open Filter Topology PhysicsLogic.Paradigm.OrderedLimits

example : ∀ (response : Nat -> Real -> Real) (value : Real),
    (ObservableLimitFamily.mk response atTop
      (nhdsWithin (0 : Real) (Set.Ioi 0))).HasFirstThenSecondLimitAt value ↔
      ∃ intermediate : Real -> Real,
        (∃ delta > 0, ∀ field, 0 < field -> field < delta ->
          ∀ epsilon > 0, ∃ cutoff : Nat, ∀ size, cutoff ≤ size ->
            |response size field - intermediate field| < epsilon) ∧
        (∀ epsilon > 0, ∃ delta > 0, ∀ field,
          0 < field -> field < delta -> |intermediate field - value| < epsilon) :=
  volume_then_field_limit_iff_explicit_cutoffs

example : ∀ (response : Nat -> Real -> Real) (value : Real),
    (ObservableLimitFamily.mk response atTop
      (nhdsWithin (0 : Real) (Set.Ioi 0))).swap.HasFirstThenSecondLimitAt value ↔
      ∃ intermediate : Nat -> Real,
        (∃ cutoff : Nat, ∀ size, cutoff ≤ size ->
          ∀ epsilon > 0, ∃ delta > 0, ∀ field,
            0 < field -> field < delta -> |response size field - intermediate size| < epsilon) ∧
        (∀ epsilon > 0, ∃ cutoff : Nat, ∀ size,
          cutoff ≤ size -> |intermediate size - value| < epsilon) :=
  field_then_volume_limit_iff_explicit_cutoffs

#print axioms volume_then_field_limit_iff_explicit_cutoffs
#print axioms field_then_volume_limit_iff_explicit_cutoffs