topology.sets.closeds - mathlib3 docs

source

structure topological_space.closeds (α : Type u_4) [topological_space α] :

Type u_4

carrier : set α
closed' : is_closed self.carrier

The type of closed subsets of a topological space.

Instances for topological_space.closeds

topological_space.closeds.has_sizeof_inst
topological_space.closeds.set_like
topological_space.closeds.complete_lattice
topological_space.closeds.inhabited
topological_space.closeds.order.coframe

source

@[protected, instance]

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

set_like (topological_space.closeds α) α

Equations

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

source

theorem topological_space.closeds.closed {α : Type u_2} [topological_space α] (s : topological_space.closeds α) :

is_closed ↑s

source

@[protected, ext]

theorem topological_space.closeds.ext {α : Type u_2} [topological_space α] {s t : topological_space.closeds α} (h : ↑s = ↑t) :

s = t

source

@[simp]

theorem topological_space.closeds.coe_mk {α : Type u_2} [topological_space α] (s : set α) (h : is_closed s) :

↑{carrier := s, closed' := h} = s

source

@[protected]

def topological_space.closeds.closure {α : Type u_2} [topological_space α] (s : set α) :

topological_space.closeds α

The closure of a set, as an element of closeds.

Equations

topological_space.closeds.closure s = {carrier := closure s, closed' := _}

source

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

galois_connection topological_space.closeds.closure coe

source

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

galois_insertion topological_space.closeds.closure coe

The galois coinsertion between sets and opens.

Equations

topological_space.closeds.gi = {choice := λ (s : set α) (hs : ↑(topological_space.closeds.closure s) ≤ s), {carrier := s, closed' := _}, gc := _, le_l_u := _, choice_eq := _}

source

@[protected, instance]

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

complete_lattice (topological_space.closeds α)

Equations

topological_space.closeds.complete_lattice = topological_space.closeds.gi.lift_complete_lattice.copy complete_lattice.le topological_space.closeds.complete_lattice._proof_1 {carrier := set.univ α, closed' := _} topological_space.closeds.complete_lattice._proof_2 {carrier := ∅, closed' := _} topological_space.closeds.complete_lattice._proof_3 (λ (s t : topological_space.closeds α), {carrier := ↑s ∪ ↑t, closed' := _}) topological_space.closeds.complete_lattice._proof_5 (λ (s t : topological_space.closeds α), {carrier := ↑s ∩ ↑t, closed' := _}) topological_space.closeds.complete_lattice._proof_7 complete_lattice.Sup topological_space.closeds.complete_lattice._proof_8 (λ (S : set (topological_space.closeds α)), {carrier := ⋂ (s : topological_space.closeds α) (H : s ∈ S), ↑s, closed' := _}) topological_space.closeds.complete_lattice._proof_10

source

@[protected, instance]

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

inhabited (topological_space.closeds α)

The type of closed sets is inhabited, with default element the empty set.

Equations

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

source

@[simp, norm_cast]

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

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

source

@[simp, norm_cast]

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

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

source

@[simp, norm_cast]

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

↑⊤ = set.univ

source

@[simp, norm_cast]

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

↑⊥ = ∅

source

@[simp, norm_cast]

theorem topological_space.closeds.coe_Inf {α : Type u_2} [topological_space α] {S : set (topological_space.closeds α)} :

↑(has_Inf.Inf S) = ⋂ (i : topological_space.closeds α) (H : i ∈ S), ↑i

source

@[simp, norm_cast]

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

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

source

@[simp, norm_cast]

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

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

source

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

(⨅ (i : ι), s i) = {carrier := ⋂ (i : ι), ↑(s i), closed' := _}

source

@[simp]

theorem topological_space.closeds.infi_mk {α : Type u_2} [topological_space α] {ι : Sort u_1} (s : ι → set α) (h : ∀ (i : ι), is_closed (s i)) :

(⨅ (i : ι), {carrier := s i, closed' := _}) = {carrier := ⋂ (i : ι), s i, closed' := _}

source

@[simp, norm_cast]

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

(↑⨅ (i : ι), s i) = ⋂ (i : ι), ↑(s i)

source

@[simp]

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

x ∈ infi s ↔ ∀ (i : ι), x ∈ s i

source

@[simp]

theorem topological_space.closeds.mem_Inf {α : Type u_2} [topological_space α] {S : set (topological_space.closeds α)} {x : α} :

x ∈ has_Inf.Inf S ↔ ∀ (s : topological_space.closeds α), s ∈ S → x ∈ s

source

@[protected, instance]

def topological_space.closeds.order.coframe {α : Type u_2} [topological_space α] :

order.coframe (topological_space.closeds α)

Equations

topological_space.closeds.order.coframe = {sup := complete_lattice.sup topological_space.closeds.complete_lattice, le := complete_lattice.le topological_space.closeds.complete_lattice, lt := complete_lattice.lt topological_space.closeds.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.closeds.complete_lattice, inf_le_left := _, inf_le_right := _, le_inf := _, Sup := complete_lattice.Sup topological_space.closeds.complete_lattice, le_Sup := _, Sup_le := _, Inf := has_Inf.Inf (conditionally_complete_lattice.to_has_Inf (topological_space.closeds α)), Inf_le := _, le_Inf := _, top := complete_lattice.top topological_space.closeds.complete_lattice, bot := complete_lattice.bot topological_space.closeds.complete_lattice, le_top := _, bot_le := _, infi_sup_le_sup_Inf := _}

source

@[simp]

theorem topological_space.closeds.singleton_carrier {α : Type u_2} [topological_space α] [t1_space α] (x : α) :

(topological_space.closeds.singleton x).carrier = {x}

source

def topological_space.closeds.singleton {α : Type u_2} [topological_space α] [t1_space α] (x : α) :

topological_space.closeds α

The term of closeds α corresponding to a singleton.

Equations

topological_space.closeds.singleton x = {carrier := {x}, closed' := _}

source

@[simp]

theorem topological_space.closeds.compl_coe {α : Type u_2} [topological_space α] (s : topological_space.closeds α) :

↑(s.compl) = (↑s)ᶜ

source

def topological_space.closeds.compl {α : Type u_2} [topological_space α] (s : topological_space.closeds α) :

topological_space.opens α

The complement of a closed set as an open set.

Equations

s.compl = {carrier := (↑s)ᶜ, is_open' := _}

source

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

topological_space.closeds α

The complement of an open set as a closed set.

Equations

s.compl = {carrier := (↑s)ᶜ, closed' := _}

source

@[simp]

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

s.compl.carrier = (↑s)ᶜ

source

theorem topological_space.closeds.compl_compl {α : Type u_2} [topological_space α] (s : topological_space.closeds α) :

s.compl.compl = s

source

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

s.compl.compl = s

source

theorem topological_space.closeds.compl_bijective {α : Type u_2} [topological_space α] :

function.bijective topological_space.closeds.compl

source

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

function.bijective topological_space.opens.compl

source

@[simp]

theorem topological_space.closeds.compl_order_iso_symm_apply (α : Type u_2) [topological_space α] (ᾰ : (topological_space.opens α)ᵒᵈ) :

⇑(rel_iso.symm (topological_space.closeds.compl_order_iso α)) ᾰ = (topological_space.opens.compl ∘ ⇑order_dual.of_dual) ᾰ

source

def topological_space.closeds.compl_order_iso (α : Type u_2) [topological_space α] :

topological_space.closeds α ≃o (topological_space.opens α)ᵒᵈ

closeds.compl as an order_iso to the order dual of opens α.

Equations

topological_space.closeds.compl_order_iso α = {to_equiv := {to_fun := ⇑order_dual.to_dual ∘ topological_space.closeds.compl, inv_fun := topological_space.opens.compl ∘ ⇑order_dual.of_dual, left_inv := _, right_inv := _}, map_rel_iff' := _}

source

@[simp]

theorem topological_space.closeds.compl_order_iso_apply (α : Type u_2) [topological_space α] (ᾰ : topological_space.closeds α) :

⇑(topological_space.closeds.compl_order_iso α) ᾰ = (⇑order_dual.to_dual ∘ topological_space.closeds.compl) ᾰ

source

@[simp]

theorem topological_space.opens.compl_order_iso_apply (α : Type u_2) [topological_space α] (ᾰ : topological_space.opens α) :

⇑(topological_space.opens.compl_order_iso α) ᾰ = (⇑order_dual.to_dual ∘ topological_space.opens.compl) ᾰ

source

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

topological_space.opens α ≃o (topological_space.closeds α)ᵒᵈ

opens.compl as an order_iso to the order dual of closeds α.

Equations

topological_space.opens.compl_order_iso α = {to_equiv := {to_fun := ⇑order_dual.to_dual ∘ topological_space.opens.compl, inv_fun := topological_space.closeds.compl ∘ ⇑order_dual.of_dual, left_inv := _, right_inv := _}, map_rel_iff' := _}

source

@[simp]

theorem topological_space.opens.compl_order_iso_symm_apply (α : Type u_2) [topological_space α] (ᾰ : (topological_space.closeds α)ᵒᵈ) :

⇑(rel_iso.symm (topological_space.opens.compl_order_iso α)) ᾰ = (topological_space.closeds.compl ∘ ⇑order_dual.of_dual) ᾰ

source

theorem topological_space.closeds.is_atom_iff {α : Type u_2} [topological_space α] [t1_space α] {s : topological_space.closeds α} :

is_atom s ↔ ∃ (x : α), s = topological_space.closeds.singleton x

in a t1_space, atoms of closeds α are precisely the closeds.singletons.

source

theorem topological_space.opens.is_coatom_iff {α : Type u_2} [topological_space α] [t1_space α] {s : topological_space.opens α} :

is_coatom s ↔ ∃ (x : α), s = (topological_space.closeds.singleton x).compl

in a t1_space, coatoms of opens α are precisely complements of singletons: (closeds.singleton x).compl.

source

structure topological_space.clopens (α : Type u_4) [topological_space α] :

Type u_4

carrier : set α
clopen' : is_clopen self.carrier

The type of clopen sets of a topological space.

Instances for topological_space.clopens

topological_space.clopens.has_sizeof_inst
topological_space.clopens.set_like
topological_space.clopens.has_sup
topological_space.clopens.has_inf
topological_space.clopens.has_top
topological_space.clopens.has_bot
topological_space.clopens.has_sdiff
topological_space.clopens.has_compl
topological_space.clopens.boolean_algebra
topological_space.clopens.inhabited

source

@[protected, instance]

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

set_like (topological_space.clopens α) α

Equations

topological_space.clopens.set_like = {coe := λ (s : topological_space.clopens α), s.carrier, coe_injective' := _}

source

theorem topological_space.clopens.clopen {α : Type u_2} [topological_space α] (s : topological_space.clopens α) :

is_clopen ↑s

source

@[simp]

theorem topological_space.clopens.to_opens_coe {α : Type u_2} [topological_space α] (s : topological_space.clopens α) :

↑(s.to_opens) = ↑s

source

def topological_space.clopens.to_opens {α : Type u_2} [topological_space α] (s : topological_space.clopens α) :

topological_space.opens α

Reinterpret a compact open as an open.

Equations

s.to_opens = {carrier := ↑s, is_open' := _}

source

@[protected, ext]

theorem topological_space.clopens.ext {α : Type u_2} [topological_space α] {s t : topological_space.clopens α} (h : ↑s = ↑t) :

s = t

source

@[simp]

theorem topological_space.clopens.coe_mk {α : Type u_2} [topological_space α] (s : set α) (h : is_clopen s) :

↑{carrier := s, clopen' := h} = s

source

@[protected, instance]

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

has_sup (topological_space.clopens α)

Equations

topological_space.clopens.has_sup = {sup := λ (s t : topological_space.clopens α), {carrier := ↑s ∪ ↑t, clopen' := _}}

source

@[protected, instance]

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

has_inf (topological_space.clopens α)

Equations

topological_space.clopens.has_inf = {inf := λ (s t : topological_space.clopens α), {carrier := ↑s ∩ ↑t, clopen' := _}}

source

@[protected, instance]

def topological_space.clopens.has_top {α : Type u_2} [topological_space α] :

has_top (topological_space.clopens α)

Equations

topological_space.clopens.has_top = {top := {carrier := ⊤, clopen' := _}}

source

@[protected, instance]

def topological_space.clopens.has_bot {α : Type u_2} [topological_space α] :

has_bot (topological_space.clopens α)

Equations

topological_space.clopens.has_bot = {bot := {carrier := ⊥, clopen' := _}}

source

@[protected, instance]

def topological_space.clopens.has_sdiff {α : Type u_2} [topological_space α] :

has_sdiff (topological_space.clopens α)

Equations

topological_space.clopens.has_sdiff = {sdiff := λ (s t : topological_space.clopens α), {carrier := ↑s \ ↑t, clopen' := _}}

source

@[protected, instance]

def topological_space.clopens.has_compl {α : Type u_2} [topological_space α] :

has_compl (topological_space.clopens α)

Equations

topological_space.clopens.has_compl = {compl := λ (s : topological_space.clopens α), {carrier := (↑s)ᶜ, clopen' := _}}

source

@[protected, instance]

def topological_space.clopens.boolean_algebra {α : Type u_2} [topological_space α] :

boolean_algebra (topological_space.clopens α)

Equations

topological_space.clopens.boolean_algebra = function.injective.boolean_algebra coe topological_space.clopens.boolean_algebra._proof_1 topological_space.clopens.boolean_algebra._proof_2 topological_space.clopens.boolean_algebra._proof_3 topological_space.clopens.boolean_algebra._proof_4 topological_space.clopens.boolean_algebra._proof_5 topological_space.clopens.boolean_algebra._proof_6 topological_space.clopens.boolean_algebra._proof_7

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

↑⊤ = set.univ

source

@[simp]

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

↑⊥ = ∅

source

@[simp]

theorem topological_space.clopens.coe_sdiff {α : Type u_2} [topological_space α] (s t : topological_space.clopens α) :

↑(s \ t) = ↑s \ ↑t

source

@[simp]

theorem topological_space.clopens.coe_compl {α : Type u_2} [topological_space α] (s : topological_space.clopens α) :

↑sᶜ = (↑s)ᶜ

source

@[protected, instance]

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

inhabited (topological_space.clopens α)

Equations

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

mathlib3 documentation

Closed sets #

Main Definitions #

Closed sets #

Clopen sets #