order topology

Stream: maths

[Kevin Kappelmann]

I did some convergence proof of a sequence using the standard epsilontics approach. I then asked @Patrick Massot how to use fabulous filters instead, and we ended up writing these definitions/instances and lemma:

local notation `|` x `|` := abs x
variable {α : Type*}

namespace partial_order
section topology
open topological_space set
variable [partial_order α]

def topology : topological_space α :=
generate_from {s : set α | ∃ (a : α), s = {b : α | a < b} ∨ s = {b : α | b < a}}

local attribute [instance] topology

def order_topology : orderable_topology α := ⟨rfl⟩
end topology
end partial_order

namespace decidable_linear_ordered_comm_group
variable [decidable_linear_ordered_comm_group α]
local attribute [instance] partial_order.topology
local attribute [instance] partial_order.order_topology

lemma order_topology.tendsto_iff_epsilon {β : Type*} (f : β → α) (z : filter β) (a : α) :
  filter.tendsto f z (nhds a) ↔ ∀ ε > (0 : α), {b : β | |f b - a| < ε} ∈ z :=
begin
  rw (show _, from @tendsto_orderable α), -- does not work without `show` for some reason
  split,
  { rintros ⟨hyp_lt_a, hyp_gt_a⟩ ε ε_pos,
    suffices : {b : β | f b - a < ε ∧ a - f b < ε} ∈ z, by simpa only [abs_sub_lt_iff],
    have set1 : {b : β | a - f b < ε} ∈ z, by
    { have : {b : β | a - ε < f b} ∈ z, from hyp_lt_a (a - ε) (sub_lt_self a ε_pos),
      have : ∀ b, a - f b < ε ↔ a - ε < f b, by { intro _, exact sub_lt },
      simpa only [this] },
    have set2 : {b : β | f b - a < ε} ∈ z, by
    { have : {b : β | a + ε > f b} ∈ z, from hyp_gt_a (a + ε) (lt_add_of_pos_right a ε_pos),
      have : ∀ b, f b - a < ε ↔ a + ε > f b, by { intro _, exact sub_lt_iff_lt_add' },
      simpa only [this] },
    exact (z.inter_sets set2 set1) },
  { assume hyp_ε_pos,
    split,
    { assume a' a'_lt_a,
      let ε := a - a',
      have : {b : β | |f b - a| < ε} ∈ z, from hyp_ε_pos ε (sub_pos.elim_right a'_lt_a),
      have : {b : β | f b - a < ε ∧ a - f b < ε} ∈ z, by simpa only [abs_sub_lt_iff] using this,
      have : {b : β | a - f b < ε} ∈ z, from z.sets_of_superset this (set.inter_subset_right _ _),
      have : ∀ b, a' < f b ↔ a - f b < ε, by {intro b, rw [sub_lt, sub_sub_self] },
      simpa only [this] },
    { assume a' a'_gt_a,
      let ε := a' - a,
      have : {b : β | |f b - a| < ε} ∈ z, from hyp_ε_pos ε (sub_pos.elim_right a'_gt_a),
      have : {b : β | f b - a < ε ∧ a - f b < ε} ∈ z, by simpa only [abs_sub_lt_iff] using this,
      have : {b : β | f b - a < ε} ∈ z, from z.sets_of_superset this (set.inter_subset_left _ _),
      have : ∀ b, a' > f b ↔ f b - a < ε, by {intro b, simp [lt_sub_iff_add_lt] },
      simpa only [this] }}
end

end decidable_linear_ordered_comm_group

I have no clue about Lean's topology library. Should this all live in mathlib? If so, where? Are there duplicates?