mathlib documentation

topology.sets.opens

Open sets #

Summary #

We define the subtype of open sets in a topological space.

Main Definitions #

source
def topological_space.opens (α : Type u_2) [topological_space α] :
Type u_2

The type of open subsets of a topological space.

Equations
Instances for topological_space.opens
source
@[protected, instance]
def topological_space.opens.set.has_coe {α : Type u_2} [topological_space α] :
has_coe (topological_space.opens α) (set α)
Equations
source
theorem topological_space.opens.val_eq_coe {α : Type u_2} [topological_space α] (U : topological_space.opens α) :
U.val = ↑U
source
theorem topological_space.opens.coe_mk {α : Type u_1} [topological_space α] {U : set α} {hU : is_open U} :
↑⟨U, hU⟩ = U

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

source
@[protected, instance]
def topological_space.opens.has_subset {α : Type u_2} [topological_space α] :
has_subset (topological_space.opens α)
Equations
source
@[protected, instance]
def topological_space.opens.has_mem {α : Type u_2} [topological_space α] :
has_mem α (topological_space.opens α)
Equations
source
@[simp]
theorem topological_space.opens.subset_coe {α : Type u_2} [topological_space α] {U V : topological_space.opens α} :
↑U ⊆ ↑V = (U ⊆ V)
source
@[simp]
theorem topological_space.opens.mem_coe {α : Type u_2} [topological_space α] {x : α} {U : topological_space.opens α} :
x ∈ ↑U = (x ∈ U)
source
@[simp]
theorem topological_space.opens.mem_mk {α : Type u_2} [topological_space α] {x : α} {U : set α} {h : is_open U} :
x ∈ ⟨U, h⟩ ↔ x ∈ U
source
@[ext]
theorem topological_space.opens.ext {α : Type u_2} [topological_space α] {U V : topological_space.opens α} (h : ↑U = ↑V) :
U = V
source
@[ext]
theorem topological_space.opens.ext_iff {α : Type u_2} [topological_space α] {U V : topological_space.opens α} :
↑U = ↑V ↔ U = V
source
@[protected, instance]
def topological_space.opens.partial_order {α : Type u_2} [topological_space α] :
partial_order (topological_space.opens α)
Equations
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
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 subtype.val topological_space.opens.interior

The galois coinsertion between sets and opens.

Equations
source
@[protected, instance]
def topological_space.opens.complete_lattice {α : Type u_2} [topological_space α] :
complete_lattice (topological_space.opens α)
Equations
source
theorem topological_space.opens.le_def {α : Type u_2} [topological_space α] {U V : topological_space.opens α} :
U ≤ V ↔ ↑U ≤ ↑V
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} :
⟨U, hU⟩ ⊓ ⟨V, hV⟩ = ⟨U ⊓ V, _⟩
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.has_inter {α : Type u_2} [topological_space α] :
has_inter (topological_space.opens α)
Equations
source
@[protected, instance]
def topological_space.opens.has_union {α : Type u_2} [topological_space α] :
has_union (topological_space.opens α)
Equations
source
@[protected, instance]
def topological_space.opens.has_emptyc {α : Type u_2} [topological_space α] :
has_emptyc (topological_space.opens α)
Equations
source
@[protected, instance]
def topological_space.opens.inhabited {α : Type u_2} [topological_space α] :
inhabited (topological_space.opens α)
Equations
source
@[simp]
theorem topological_space.opens.inter_eq {α : Type u_2} [topological_space α] (U V : topological_space.opens α) :
U ∩ V = U ⊓ V
source
@[simp]
theorem topological_space.opens.union_eq {α : Type u_2} [topological_space α] (U V : topological_space.opens α) :
U ∪ V = U ⊔ V
source
@[simp]
theorem topological_space.opens.empty_eq {α : Type u_2} [topological_space α] :
∅ = ⊥
source
theorem topological_space.opens.supr_def {α : Type u_2} [topological_space α] {ι : Sort u_1} (s : ι → topological_space.opens α) :
(⨆ (i : ι), s i) = ⟨⋃ (i : ι), ↑(s i), _⟩
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 : ι), ⟨s i, _⟩) = ⟨⋃ (i : ι), s i, _⟩
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
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
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_compact_open_iff_eq_finite_Union_of_is_basis {α : 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
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
@[simp]
theorem topological_space.opens.comap_val {α : Type u_2} {β : Type u_3} [topological_space α] [topological_space β] (f : C(α, β)) (U : topological_space.opens β) :
(⇑(topological_space.opens.comap f) U).val = ⇑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
@[protected, simp]
def topological_space.opens.equiv {α : Type u_2} {β : Type u_3} [topological_space α] [topological_space β] (f : α ≃ₜ β) :
topological_space.opens α ≃ topological_space.opens β

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

Equations
source
@[protected, simp]
def topological_space.opens.order_iso {α : Type u_2} {β : Type u_3} [topological_space α] [topological_space β] (f : α ≃ₜ β) :
topological_space.opens α ≃o topological_space.opens β

A homeomorphism induces an order isomorphism on open sets, by taking comaps.

Equations
source
def topological_space.open_nhds_of {α : Type u_2} [topological_space α] (x : α) :
Type u_2

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

Equations
Instances for topological_space.open_nhds_of
source
@[protected, instance]
def topological_space.open_nhds_of.inhabited {α : Type u_1} [topological_space α] (x : α) :
inhabited (topological_space.open_nhds_of x)
Equations
source
@[protected, instance]
def topological_space.opens.finite {α : Type u_2} [topological_space α] [finite α] :
finite (topological_space.opens α)