Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Merged by Bors] - feat(LowerUpperTopology): add lemmas #20465

Closed
wants to merge 1 commit into from
Closed

[Merged by Bors] - feat(LowerUpperTopology): add lemmas #20465

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
57 changes: 53 additions & 4 deletions Mathlib/Topology/Order/LowerUpperTopology.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -102,16 +102,32 @@ protected def rec {β : WithLower α → Sort*} (h : ∀ a, β (toLower a)) :
instance [Nonempty α] : Nonempty (WithLower α) := ‹Nonempty α›
instance [Inhabited α] : Inhabited (WithLower α) := ‹Inhabited α›

section Preorder

variable [Preorder α] {s : Set α}

instance : Preorder (WithLower α) := ‹Preorder α›
instance : TopologicalSpace (WithLower α) := lower α
instance : TopologicalSpace (WithLower α) := lower (WithLower α)

@[simp] lemma toLower_le_toLower {x y : α} : toLower x ≤ toLower y ↔ x ≤ y := .rfl
@[simp] lemma toLower_lt_toLower {x y : α} : toLower x < toLower y ↔ x < y := .rfl
@[simp] lemma ofLower_le_ofLower {x y : WithLower α} : ofLower x ≤ ofLower y ↔ x ≤ y := .rfl
@[simp] lemma ofLower_lt_ofLower {x y : WithLower α} : ofLower x < ofLower y ↔ x < y := .rfl

lemma isOpen_preimage_ofLower : IsOpen (ofLower ⁻¹' s) ↔ (lower α).IsOpen s := Iff.rfl
lemma isOpen_preimage_ofLower : IsOpen (ofLower ⁻¹' s) ↔ IsOpen[lower α] s := Iff.rfl

lemma isOpen_def (T : Set (WithLower α)) : IsOpen T ↔ (lower α).IsOpen (WithLower.toLower ⁻¹' T) :=
lemma isOpen_def (T : Set (WithLower α)) : IsOpen T ↔ IsOpen[lower α] (WithLower.toLower ⁻¹' T) :=
Iff.rfl

theorem continuous_toLower [TopologicalSpace α] [ClosedIciTopology α] :
Continuous (toLower : α → WithLower α) :=
continuous_generateFrom_iff.mpr <| by rintro _ ⟨a, rfl⟩; exact isClosed_Ici.isOpen_compl

end Preorder

instance [PartialOrder α] : PartialOrder (WithLower α) := ‹PartialOrder α›
instance [LinearOrder α] : LinearOrder (WithLower α) := ‹LinearOrder α›

end WithLower

/-- Type synonym for a preorder equipped with the upper topology. -/
Expand Down Expand Up @@ -141,15 +157,31 @@ protected def rec {β : WithUpper α → Sort*} (h : ∀ a, β (toUpper a)) :
instance [Nonempty α] : Nonempty (WithUpper α) := ‹Nonempty α›
instance [Inhabited α] : Inhabited (WithUpper α) := ‹Inhabited α›

section Preorder

variable [Preorder α] {s : Set α}

instance : Preorder (WithUpper α) := ‹Preorder α›
instance : TopologicalSpace (WithUpper α) := upper α
instance : TopologicalSpace (WithUpper α) := upper (WithUpper α)

@[simp] lemma toUpper_le_toUpper {x y : α} : toUpper x ≤ toUpper y ↔ x ≤ y := .rfl
@[simp] lemma toUpper_lt_toUpper {x y : α} : toUpper x < toUpper y ↔ x < y := .rfl
@[simp] lemma ofUpper_le_ofUpper {x y : WithUpper α} : ofUpper x ≤ ofUpper y ↔ x ≤ y := .rfl
@[simp] lemma ofUpper_lt_ofUpper {x y : WithUpper α} : ofUpper x < ofUpper y ↔ x < y := .rfl

lemma isOpen_preimage_ofUpper : IsOpen (ofUpper ⁻¹' s) ↔ (upper α).IsOpen s := Iff.rfl

lemma isOpen_def {s : Set (WithUpper α)} : IsOpen s ↔ (upper α).IsOpen (toUpper ⁻¹' s) := Iff.rfl

theorem continuous_toUpper [TopologicalSpace α] [ClosedIicTopology α] :
Continuous (toUpper : α → WithUpper α) :=
continuous_generateFrom_iff.mpr <| by rintro _ ⟨a, rfl⟩; exact isClosed_Iic.isOpen_compl

end Preorder

instance [PartialOrder α] : PartialOrder (WithUpper α) := ‹PartialOrder α›
instance [LinearOrder α] : LinearOrder (WithUpper α) := ‹LinearOrder α›

end WithUpper

/--
Expand Down Expand Up @@ -236,6 +268,11 @@ theorem isLowerSet_of_isOpen (h : IsOpen s) : IsLowerSet s := by
theorem isUpperSet_of_isClosed (h : IsClosed s) : IsUpperSet s :=
isLowerSet_compl.1 <| isLowerSet_of_isOpen h.isOpen_compl

theorem tendsto_nhds_iff_not_le {β : Type*} {f : β → α} {l : Filter β} {x : α} :
Filter.Tendsto f l (𝓝 x) ↔ ∀ y, ¬y ≤ x → ∀ᶠ z in l, ¬y ≤ f z := by
simp [topology_eq_lowerTopology, tendsto_nhds_generateFrom_iff, Filter.Eventually, Ici,
compl_setOf]

/--
The closure of a singleton `{a}` in the lower topology is the left-closed right-infinite interval
[a, ∞).
Expand Down Expand Up @@ -292,6 +329,10 @@ lemma isTopologicalBasis_insert_univ_subbasis :
use b ⊓ c
rw [compl_Ici, compl_Ici, compl_Ici, Iio_inter_Iio])

theorem tendsto_nhds_iff_lt {β : Type*} {f : β → α} {l : Filter β} {x : α} :
Filter.Tendsto f l (𝓝 x) ↔ ∀ y, x < y → ∀ᶠ z in l, f z < y := by
simp only [tendsto_nhds_iff_not_le, not_le]

end LinearOrder

section CompleteLinearOrder
Expand Down Expand Up @@ -382,6 +423,10 @@ theorem isUpperSet_of_isOpen (h : IsOpen s) : IsUpperSet s :=
theorem isLowerSet_of_isClosed (h : IsClosed s) : IsLowerSet s :=
isUpperSet_compl.1 <| isUpperSet_of_isOpen h.isOpen_compl

theorem tendsto_nhds_iff_not_le {β : Type*} {f : β → α} {l : Filter β} {x : α} :
Filter.Tendsto f l (𝓝 x) ↔ ∀ y, ¬x ≤ y → ∀ᶠ z in l, ¬f z ≤ y :=
IsLower.tendsto_nhds_iff_not_le (α := αᵒᵈ)

/--
The closure of a singleton `{a}` in the upper topology is the left-infinite right-closed interval
(-∞,a].
Expand Down Expand Up @@ -421,6 +466,10 @@ lemma isTopologicalBasis_insert_univ_subbasis :
IsTopologicalBasis (insert univ {s : Set α | ∃ a, (Iic a)ᶜ = s}) :=
IsLower.isTopologicalBasis_insert_univ_subbasis (α := αᵒᵈ)

theorem tendsto_nhds_iff_lt {β : Type*} {f : β → α} {l : Filter β} {x : α} :
Filter.Tendsto f l (𝓝 x) ↔ ∀ y < x, ∀ᶠ z in l, y < f z :=
IsLower.tendsto_nhds_iff_lt (α := αᵒᵈ)

end LinearOrder

section CompleteLinearOrder
Expand Down
Loading