topology.sets.opens - mathlib docs

source

structure topological_space.opens (α : Type u_2) [topological_space α] :

Type u_2

carrier : set α
is_open' : is_open self.carrier

The type of open subsets of a topological space.

Instances for topological_space.opens

topological_space.opens.has_sizeof_inst
topological_space.opens.set_like
topological_space.opens.is_open.can_lift
topological_space.opens.complete_lattice
topological_space.opens.inhabited
topological_space.opens.order.frame
topological_space.opens.finite
open_subgroup.has_coe_opens
open_add_subgroup.has_coe_opens

source

@[protected, instance]

def topological_space.opens.set_like {α : Type u_2} [topological_space α] :

set_like (topological_space.opens α) α

Equations

topological_space.opens.set_like = {coe := topological_space.opens.carrier _inst_1, coe_injective' := _}

source

@[protected, instance]

def topological_space.opens.is_open.can_lift {α : Type u_2} [topological_space α] :

can_lift (set α) (topological_space.opens α) coe is_open

Equations

topological_space.opens.is_open.can_lift = {prf := _}

source

theorem topological_space.opens.forall {α : Type u_2} [topological_space α] {p : topological_space.opens α → Prop} :

(∀ (U : topological_space.opens α), p U) ↔ ∀ (U : set α) (hU : is_open U), p {carrier := U, is_open' := hU}

source

@[simp]

theorem topological_space.opens.carrier_eq_coe {α : Type u_2} [topological_space α] (U : topological_space.opens α) :

U.carrier = ↑U

source

@[simp]

theorem topological_space.opens.coe_mk {α : Type u_2} [topological_space α] {U : set α} {hU : is_open U} :

↑{carrier := U, is_open' := hU} = U

the coercion opens α → set α applied to a pair is the same as taking the first component

source

@[simp]

theorem topological_space.opens.mem_mk {α : Type u_2} [topological_space α] {x : α} {U : set α} {h : is_open U} :

x ∈ {carrier := U, is_open' := h} ↔ x ∈ U

source

@[protected, simp]

theorem topological_space.opens.nonempty_coe_sort {α : Type u_2} [topological_space α] {U : topological_space.opens α} :

nonempty ↥U ↔ ↑U.nonempty

source

@[ext]

theorem topological_space.opens.ext {α : Type u_2} [topological_space α] {U V : topological_space.opens α} (h : ↑U = ↑V) :

U = V

source

@[simp]

theorem topological_space.opens.coe_inj {α : Type u_2} [topological_space α] {U V : topological_space.opens α} :

↑U = ↑V ↔ U = V

source

@[protected]

theorem topological_space.opens.is_open {α : Type u_2} [topological_space α] (U : topological_space.opens α) :

is_open ↑U

source

@[simp]

theorem topological_space.opens.mk_coe {α : Type u_2} [topological_space α] (U : topological_space.opens α) :

{carrier := ↑U, is_open' := _} = U

source

def topological_space.opens.simps.coe {α : Type u_2} [topological_space α] (U : topological_space.opens α) :

set α

See Note [custom simps projection].

Equations

topological_space.opens.simps.coe U = ↑U

source

def topological_space.opens.interior {α : Type u_2} [topological_space α] (s : set α) :

topological_space.opens α

The interior of a set, as an element of opens.

Equations

topological_space.opens.interior s = {carrier := interior s, is_open' := _}

source

theorem topological_space.opens.gc {α : Type u_2} [topological_space α] :

galois_connection coe topological_space.opens.interior

source

def topological_space.opens.gi {α : Type u_2} [topological_space α] :

galois_coinsertion coe topological_space.opens.interior

The galois coinsertion between sets and opens.

Equations

topological_space.opens.gi = {choice := λ (s : set α) (hs : s ≤ ↑(topological_space.opens.interior s)), {carrier := s, is_open' := _}, gc := _, u_l_le := _, choice_eq := _}

source

@[protected, instance]

def topological_space.opens.complete_lattice {α : Type u_2} [topological_space α] :

complete_lattice (topological_space.opens α)

Equations

topological_space.opens.complete_lattice = topological_space.opens.gi.lift_complete_lattice.copy (λ (U V : topological_space.opens α), ↑U ⊆ ↑V) topological_space.opens.complete_lattice._proof_1 {carrier := set.univ α, is_open' := _} topological_space.opens.complete_lattice._proof_2 {carrier := ∅, is_open' := _} topological_space.opens.complete_lattice._proof_3 (λ (U V : topological_space.opens α), {carrier := ↑U ∪ ↑V, is_open' := _}) topological_space.opens.complete_lattice._proof_5 (λ (U V : topological_space.opens α), {carrier := ↑U ∩ ↑V, is_open' := _}) topological_space.opens.complete_lattice._proof_7 (λ (S : set (topological_space.opens α)), {carrier := ⋃ (s : topological_space.opens α) (H : s ∈ S), ↑s, is_open' := _}) topological_space.opens.complete_lattice._proof_9 complete_lattice.Inf topological_space.opens.complete_lattice._proof_10

source

@[simp]

theorem topological_space.opens.mk_inf_mk {α : Type u_2} [topological_space α] {U V : set α} {hU : is_open U} {hV : is_open V} :

{carrier := U, is_open' := hU} ⊓ {carrier := V, is_open' := hV} = {carrier := U ⊓ V, is_open' := _}

source

@[simp, norm_cast]

theorem topological_space.opens.coe_inf {α : Type u_2} [topological_space α] (s t : topological_space.opens α) :

↑(s ⊓ t) = ↑s ∩ ↑t

source

@[simp, norm_cast]

theorem topological_space.opens.coe_sup {α : Type u_2} [topological_space α] (s t : topological_space.opens α) :

↑(s ⊔ t) = ↑s ∪ ↑t

source

@[simp, norm_cast]

theorem topological_space.opens.coe_bot {α : Type u_2} [topological_space α] :

↑⊥ = ∅

source

@[simp, norm_cast]

theorem topological_space.opens.coe_top {α : Type u_2} [topological_space α] :

↑⊤ = set.univ

source

@[simp, norm_cast]

theorem topological_space.opens.coe_Sup {α : Type u_2} [topological_space α] {S : set (topological_space.opens α)} :

↑(has_Sup.Sup S) = ⋃ (i : topological_space.opens α) (H : i ∈ S), ↑i

source

@[simp, norm_cast]

theorem topological_space.opens.coe_finset_sup {ι : Type u_1} {α : Type u_2} [topological_space α] (f : ι → topological_space.opens α) (s : finset ι) :

↑(s.sup f) = s.sup (coe ∘ f)

source

@[simp, norm_cast]

theorem topological_space.opens.coe_finset_inf {ι : Type u_1} {α : Type u_2} [topological_space α] (f : ι → topological_space.opens α) (s : finset ι) :

↑(s.inf f) = s.inf (coe ∘ f)

source

@[protected, instance]

def topological_space.opens.inhabited {α : Type u_2} [topological_space α] :

inhabited (topological_space.opens α)

Equations

topological_space.opens.inhabited = {default := ⊥}

source

theorem topological_space.opens.supr_def {α : Type u_2} [topological_space α] {ι : Sort u_1} (s : ι → topological_space.opens α) :

(⨆ (i : ι), s i) = {carrier := ⋃ (i : ι), ↑(s i), is_open' := _}

source

@[simp]

theorem topological_space.opens.supr_mk {α : Type u_2} [topological_space α] {ι : Sort u_1} (s : ι → set α) (h : ∀ (i : ι), is_open (s i)) :

(⨆ (i : ι), {carrier := s i, is_open' := _}) = {carrier := ⋃ (i : ι), s i, is_open' := _}

source

@[simp, norm_cast]

theorem topological_space.opens.coe_supr {α : Type u_2} [topological_space α] {ι : Sort u_1} (s : ι → topological_space.opens α) :

(↑⨆ (i : ι), s i) = ⋃ (i : ι), ↑(s i)

source

@[simp]

theorem topological_space.opens.mem_supr {α : Type u_2} [topological_space α] {ι : Sort u_1} {x : α} {s : ι → topological_space.opens α} :

x ∈ supr s ↔ ∃ (i : ι), x ∈ s i

source

@[simp]

theorem topological_space.opens.mem_Sup {α : Type u_2} [topological_space α] {Us : set (topological_space.opens α)} {x : α} :

x ∈ has_Sup.Sup Us ↔ ∃ (u : topological_space.opens α) (H : u ∈ Us), x ∈ u

source

@[protected, instance]

def topological_space.opens.order.frame {α : Type u_2} [topological_space α] :

order.frame (topological_space.opens α)

Equations

topological_space.opens.order.frame = {sup := complete_lattice.sup topological_space.opens.complete_lattice, le := complete_lattice.le topological_space.opens.complete_lattice, lt := complete_lattice.lt topological_space.opens.complete_lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := complete_lattice.inf topological_space.opens.complete_lattice, inf_le_left := _, inf_le_right := _, le_inf := _, Sup := has_Sup.Sup (conditionally_complete_lattice.to_has_Sup (topological_space.opens α)), le_Sup := _, Sup_le := _, Inf := complete_lattice.Inf topological_space.opens.complete_lattice, Inf_le := _, le_Inf := _, top := complete_lattice.top topological_space.opens.complete_lattice, bot := complete_lattice.bot topological_space.opens.complete_lattice, le_top := _, bot_le := _, inf_Sup_le_supr_inf := _}

source

theorem topological_space.opens.open_embedding_of_le {α : Type u_2} [topological_space α] {U V : topological_space.opens α} (i : U ≤ V) :

open_embedding (set.inclusion i)

source

theorem topological_space.opens.not_nonempty_iff_eq_bot {α : Type u_2} [topological_space α] (U : topological_space.opens α) :

¬↑U.nonempty ↔ U = ⊥

source

theorem topological_space.opens.ne_bot_iff_nonempty {α : Type u_2} [topological_space α] (U : topological_space.opens α) :

U ≠ ⊥ ↔ ↑U.nonempty

source

theorem topological_space.opens.eq_bot_or_top {α : Type u_1} [t : topological_space α] (h : t = ⊤) (U : topological_space.opens α) :

U = ⊥ ∨ U = ⊤

An open set in the indiscrete topology is either empty or the whole space.

source

def topological_space.opens.is_basis {α : Type u_2} [topological_space α] (B : set (topological_space.opens α)) :

Prop

A set of opens α is a basis if the set of corresponding sets is a topological basis.

Equations

topological_space.opens.is_basis B = topological_space.is_topological_basis (coe '' B)

source

theorem topological_space.opens.is_basis_iff_nbhd {α : Type u_2} [topological_space α] {B : set (topological_space.opens α)} :

topological_space.opens.is_basis B ↔ ∀ {U : topological_space.opens α} {x : α}, x ∈ U → (∃ (U' : topological_space.opens α) (H : U' ∈ B), x ∈ U' ∧ U' ≤ U)

source

theorem topological_space.opens.is_basis_iff_cover {α : Type u_2} [topological_space α] {B : set (topological_space.opens α)} :

topological_space.opens.is_basis B ↔ ∀ (U : topological_space.opens α), ∃ (Us : set (topological_space.opens α)) (H : Us ⊆ B), U = has_Sup.Sup Us

source

theorem topological_space.opens.is_basis.is_compact_open_iff_eq_finite_Union {α : Type u_2} [topological_space α] {ι : Type u_1} (b : ι → topological_space.opens α) (hb : topological_space.opens.is_basis (set.range b)) (hb' : ∀ (i : ι), is_compact ↑(b i)) (U : set α) :

is_compact U ∧ is_open U ↔ ∃ (s : set ι), s.finite ∧ U = ⋃ (i : ι) (H : i ∈ s), ↑(b i)

If α has a basis consisting of compact opens, then an open set in α is compact open iff it is a finite union of some elements in the basis

source

@[simp]

theorem topological_space.opens.is_compact_element_iff {α : Type u_2} [topological_space α] (s : topological_space.opens α) :

complete_lattice.is_compact_element s ↔ is_compact ↑s

source

def topological_space.opens.comap {α : Type u_2} {β : Type u_3} [topological_space α] [topological_space β] (f : C(α, β)) :

frame_hom (topological_space.opens β) (topological_space.opens α)

The preimage of an open set, as an open set.

Equations

topological_space.opens.comap f = {to_inf_top_hom := {to_inf_hom := {to_fun := λ (s : topological_space.opens β), {carrier := ⇑f ⁻¹' ↑s, is_open' := _}, map_inf' := _}, map_top' := _}, map_Sup' := _}

source

@[simp]

theorem topological_space.opens.comap_id {α : Type u_2} [topological_space α] :

topological_space.opens.comap (continuous_map.id α) = frame_hom.id (topological_space.opens α)

source

theorem topological_space.opens.comap_mono {α : Type u_2} {β : Type u_3} [topological_space α] [topological_space β] (f : C(α, β)) {s t : topological_space.opens β} (h : s ≤ t) :

⇑(topological_space.opens.comap f) s ≤ ⇑(topological_space.opens.comap f) t

source

@[simp]

theorem topological_space.opens.coe_comap {α : Type u_2} {β : Type u_3} [topological_space α] [topological_space β] (f : C(α, β)) (U : topological_space.opens β) :

↑(⇑(topological_space.opens.comap f) U) = ⇑f ⁻¹' ↑U

source

@[protected]

theorem topological_space.opens.comap_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [topological_space α] [topological_space β] [topological_space γ] (g : C(β, γ)) (f : C(α, β)) :

topological_space.opens.comap (g.comp f) = (topological_space.opens.comap f).comp (topological_space.opens.comap g)

source

@[protected]

theorem topological_space.opens.comap_comap {α : Type u_2} {β : Type u_3} {γ : Type u_4} [topological_space α] [topological_space β] [topological_space γ] (g : C(β, γ)) (f : C(α, β)) (U : topological_space.opens γ) :

⇑(topological_space.opens.comap f) (⇑(topological_space.opens.comap g) U) = ⇑(topological_space.opens.comap (g.comp f)) U

source

theorem topological_space.opens.comap_injective {α : Type u_2} {β : Type u_3} [topological_space α] [topological_space β] [t0_space β] :

function.injective topological_space.opens.comap

source

@[simp]

theorem homeomorph.opens_congr_apply {α : Type u_2} {β : Type u_3} [topological_space α] [topological_space β] (f : α ≃ₜ β) :

⇑(f.opens_congr) = ⇑(topological_space.opens.comap f.symm.to_continuous_map)

source

def homeomorph.opens_congr {α : Type u_2} {β : Type u_3} [topological_space α] [topological_space β] (f : α ≃ₜ β) :

topological_space.opens α ≃o topological_space.opens β

A homeomorphism induces an order-preserving equivalence on open sets, by taking comaps.

Equations

f.opens_congr = {to_equiv := {to_fun := ⇑(topological_space.opens.comap f.symm.to_continuous_map), inv_fun := ⇑(topological_space.opens.comap f.to_continuous_map), left_inv := _, right_inv := _}, map_rel_iff' := _}

source

@[simp]

theorem homeomorph.opens_congr_symm {α : Type u_2} {β : Type u_3} [topological_space α] [topological_space β] (f : α ≃ₜ β) :

f.opens_congr.symm = f.symm.opens_congr

source

@[protected, instance]

def topological_space.opens.finite {α : Type u_2} [topological_space α] [finite α] :

finite (topological_space.opens α)

source

structure topological_space.open_nhds_of {α : Type u_2} [topological_space α] (x : α) :

Type u_2

to_opens : topological_space.opens α
mem' : x ∈ self.to_opens.carrier

The open neighborhoods of a point. See also opens or nhds.

Instances for topological_space.open_nhds_of

topological_space.open_nhds_of.has_sizeof_inst
topological_space.open_nhds_of.set_like
topological_space.open_nhds_of.can_lift_set
topological_space.open_nhds_of.order_top
topological_space.open_nhds_of.inhabited
topological_space.open_nhds_of.has_inf
topological_space.open_nhds_of.has_sup
topological_space.open_nhds_of.distrib_lattice

source

theorem topological_space.open_nhds_of.to_opens_injective {α : Type u_2} [topological_space α] {x : α} :

function.injective topological_space.open_nhds_of.to_opens

source

@[protected, instance]

def topological_space.open_nhds_of.set_like {α : Type u_2} [topological_space α] {x : α} :

set_like (topological_space.open_nhds_of x) α

Equations

topological_space.open_nhds_of.set_like = {coe := λ (U : topological_space.open_nhds_of x), ↑(U.to_opens), coe_injective' := _}

source

@[protected, instance]

def topological_space.open_nhds_of.can_lift_set {α : Type u_2} [topological_space α] {x : α} :

can_lift (set α) (topological_space.open_nhds_of x) coe (λ (s : set α), is_open s ∧ x ∈ s)

Equations

topological_space.open_nhds_of.can_lift_set = {prf := _}

source

@[protected]

theorem topological_space.open_nhds_of.mem {α : Type u_2} [topological_space α] {x : α} (U : topological_space.open_nhds_of x) :

x ∈ U

source

@[protected]

theorem topological_space.open_nhds_of.is_open {α : Type u_2} [topological_space α] {x : α} (U : topological_space.open_nhds_of x) :

is_open ↑U

source

@[protected, instance]

def topological_space.open_nhds_of.order_top {α : Type u_2} [topological_space α] {x : α} :

order_top (topological_space.open_nhds_of x)

Equations

topological_space.open_nhds_of.order_top = {top := {to_opens := ⊤, mem' := _}, le_top := _}

source

@[protected, instance]

def topological_space.open_nhds_of.inhabited {α : Type u_2} [topological_space α] {x : α} :

inhabited (topological_space.open_nhds_of x)

Equations

topological_space.open_nhds_of.inhabited = {default := ⊤}

source

@[protected, instance]

def topological_space.open_nhds_of.has_inf {α : Type u_2} [topological_space α] {x : α} :

has_inf (topological_space.open_nhds_of x)

Equations

topological_space.open_nhds_of.has_inf = {inf := λ (U V : topological_space.open_nhds_of x), {to_opens := U.to_opens ⊓ V.to_opens, mem' := _}}

source

@[protected, instance]

def topological_space.open_nhds_of.has_sup {α : Type u_2} [topological_space α] {x : α} :

has_sup (topological_space.open_nhds_of x)

Equations

topological_space.open_nhds_of.has_sup = {sup := λ (U V : topological_space.open_nhds_of x), {to_opens := U.to_opens ⊔ V.to_opens, mem' := _}}

source

@[protected, instance]

def topological_space.open_nhds_of.distrib_lattice {α : Type u_2} [topological_space α] {x : α} :

distrib_lattice (topological_space.open_nhds_of x)

Equations

topological_space.open_nhds_of.distrib_lattice = function.injective.distrib_lattice topological_space.open_nhds_of.to_opens topological_space.open_nhds_of.to_opens_injective topological_space.open_nhds_of.distrib_lattice._proof_1 topological_space.open_nhds_of.distrib_lattice._proof_2

source

theorem topological_space.open_nhds_of.basis_nhds {α : Type u_2} [topological_space α] {x : α} :

(nhds x).has_basis (λ (U : topological_space.open_nhds_of x), true) coe

source

def topological_space.open_nhds_of.comap {α : Type u_2} {β : Type u_3} [topological_space α] [topological_space β] (f : C(α, β)) (x : α) :

lattice_hom (topological_space.open_nhds_of (⇑f x)) (topological_space.open_nhds_of x)

Preimage of an open neighborhood of f x under a continuous map f as a lattice_hom.

Equations

topological_space.open_nhds_of.comap f x = {to_sup_hom := {to_fun := λ (U : topological_space.open_nhds_of (⇑f x)), {to_opens := ⇑(topological_space.opens.comap f) U.to_opens, mem' := _}, map_sup' := _}, map_inf' := _}

source

meta def tactic.auto_cases.opens_find_tac :

expr → option tactic.auto_cases.auto_cases_tac

Find an auto_cases_tac which matches topological_space.opens.

source

meta def tactic.auto_cases_opens :

tactic string

A version of tactic.auto_cases that works for topological_space.opens.

mathlib documentation

Open sets #

Summary #

Main Definitions #

Bundled open sets #

Bundled open neighborhoods #

Main results #