## Stream: maths

### Topic: order topology

#### Kevin Kappelmann (Jul 26 2019 at 12:13):

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?

Last updated: May 11 2021 at 16:22 UTC