LeanPool.RiemannMappingTheorem.Uniform

theorem symmetricRel_of {α : Type u_2} {x : Set (α × α)} (h : ∀ {a b : α}, (a, b) ∈ x → (b, a) ∈ x) : SetRel.IsSymm x

def UniformSpace.thickening {α : Type u_2} (U : Set (α × α)) (S : Set α) : Set α

The U-thickening of S: the union of U-balls around each point of S. Equals {a | ∃ x ∈ S, (x, a) ∈ U}.

Equations

• UniformSpace.thickening U S = ⋃ x ∈ S, UniformSpace.ball x U

theorem UniformSpace.mem_thickening {α : Type u_2} {a : α} {s : Set α} {u : Set (α × α)} : a ∈ thickening u s ↔ ∃ x ∈ s, (x, a) ∈ u

@[simp]

theorem UniformSpace.thickening_singleton {α : Type u_2} {a : α} {u : Set (α × α)} : thickening u {a} = ball a u

@[simp]

theorem UniformSpace.monotone_thickening {α : Type u_2} {s : Set α} : Monotone fun (x : Set (α × α)) => thickening x s

theorem UniformSpace.thickening_mono {α : Type u_2} {u : Set (α × α)} : Monotone (thickening u)

@[simp]

theorem UniformSpace.thickening_comp {α : Type u_2} {s : Set α} {u v : Set (α × α)} : thickening v (thickening u s) = thickening (SetRel.comp u v) s

theorem UniformSpace.disjoint_ball_iff {α : Type u_2} {a : α} {t : Set α} {u : Set (α × α)} : Disjoint (ball a u) t ↔ ∀ b ∈ t, (a, b) ∉ u

theorem UniformSpace.thickening_inter_eq_empty {α : Type u_2} {s t : Set α} {u : Set (α × α)} : thickening u s ∩ t = ∅ ↔ ∀ a ∈ s, ∀ b ∈ t, (a, b) ∉ u

theorem UniformSpace.thickening_inter_eq_empty_comm {α : Type u_2} {s t : Set α} {u : Set (α × α)} (hu : SetRel.IsSymm u) : thickening u s ∩ t = ∅ ↔ s ∩ thickening u t = ∅

theorem UniformSpace.thickening_inter_thickening_eq_empty_of_comp {α : Type u_2} {s t : Set α} {u v : Set (α × α)} (hv : SetRel.IsSymm v) (hvu : SetRel.comp v v ⊆ u) (hST : thickening u s ∩ t = ∅) : thickening v s ∩ thickening v t = ∅

def uniformNhdsSet {α : Type u_2} [UniformSpace α] (s : Set α) : Filter α

The uniform neighbourhood filter of a set s: filter of supersets of U-thickenings of s for entourages U. Strengthens 𝓝ˢ s for locally uniform statements.

Equations

• uniformNhdsSet s = (uniformity α).lift' fun (x : Set (α × α)) => UniformSpace.thickening x s

def Uniformity.«term𝓝ᵘ» : Lean.ParserDescr

Notation for uniformNhdsSet, the uniform neighbourhood filter.

Equations

• Uniformity.«term𝓝ᵘ» = Lean.ParserDescr.node `Uniformity.«term𝓝ᵘ» 1024 (Lean.ParserDescr.symbol "𝓝ᵘ")

theorem UniformSpace.thickening_mem_uniform_nhds_set {α : Type u_2} {s : Set α} {u : Set (α × α)} [UniformSpace α] (hu : u ∈ uniformity α) : thickening u s ∈ uniformNhdsSet s

theorem UniformSpace.uniform_nhds_set_mono {α : Type u_2} [UniformSpace α] {s t : Set α} (h : s ⊆ t) : uniformNhdsSet s ≤ uniformNhdsSet t

theorem UniformSpace.uniform_nhds_set_singleton {α : Type u_2} [UniformSpace α] {a : α} : uniformNhdsSet {a} = nhds a

theorem UniformSpace.mem_uniform_nhds_set_iff {α : Type u_2} {s t : Set α} [UniformSpace α] : s ∈ uniformNhdsSet t ↔ ∃ u ∈ uniformity α, thickening u t ⊆ s

theorem UniformSpace.nhds_le_uniform_nhds_set {α : Type u_2} {a : α} [UniformSpace α] {s : Set α} (ha : a ∈ s) : nhds a ≤ uniformNhdsSet s

theorem UniformSpace.nhds_set_le_uniform_nhds_set {α : Type u_2} [UniformSpace α] {s : Set α} : nhdsSet s ≤ uniformNhdsSet s

theorem UniformSpace.uniform_nhds_inf_uniform_nhds_eq_bot {α : Type u_2} [UniformSpace α] {s t : Set α} (h : uniformNhdsSet s ⊓ Filter.principal t = ⊥) : uniformNhdsSet s ⊓ uniformNhdsSet t = ⊥

theorem UniformSpace.nhds_inf_uniform_nhds_eq_bot {α : Type u_2} {a : α} [UniformSpace α] {s : Set α} (hf : nhds a ⊓ Filter.principal s = ⊥) : nhds a ⊓ uniformNhdsSet s = ⊥

theorem UniformSpace.nhds_set_eq_uniform_nhds_set_of_isCompact {α : Type u_2} [UniformSpace α] {s : Set α} (hs : IsCompact s) : nhdsSet s = uniformNhdsSet s

theorem lemma0 {α : Type u_2} {s : Set α} [UniformSpace α] : Filter.Tendsto Prod.snd (uniformity α ⊓ Filter.comap Prod.fst (Filter.principal s)) (uniformNhdsSet s)

theorem lemma2 {ι : Type u_1} {α : Type u_2} {β : Type u_3} {p : Filter ι} {f : α → β} {s : Set α} : Filter.Tendsto (f ∘ Prod.snd) (p ×ˢ Filter.principal s) (Filter.principal (f '' s))

theorem lemma1 {ι : Type u_1} {α : Type u_2} {β : Type u_3} {s : Set α} {p : Filter ι} {F : ι → α → β} {f : α → β} [UniformSpace β] (hF : TendstoUniformlyOn F f p s) : Filter.Tendsto (fun (q : ι × α) => (f q.2, F q.1 q.2)) (p ×ˢ Filter.principal s) (Filter.principal (f '' s) ×ˢ uniformNhdsSet (f '' s))

theorem lemma13 {ι : Type u_1} {α : Type u_2} {β : Type u_3} {s : Set α} {p : Filter ι} {f : α → β} {F : ι → α → β} [UniformSpace β] (hF : TendstoUniformlyOn F f p s) : Filter.Tendsto (Function.uncurry F) (p ×ˢ Filter.principal s) (uniformNhdsSet (f '' s))