∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : PseudoEMetricSpace β] {n : ℕ} {j : ι} {f : ι → α → β} {g : α → β}
  [inst_1 : Preorder ι] {x : α},
  x ∈ MeasureTheory.Egorov.notConvergentSeq f g n j ↔ ∃ k ≥ j, (↑n)⁻¹ < edist (f k x) (g x)