Documentation

Mathlib.Topology.SubsetProperties

Properties of subsets of topological spaces #

In this file we define various properties of subsets of a topological space, and some classes on topological spaces.

Main definitions #

We define the following properties for sets in a topological space:

• IsCompact: each open cover has a finite subcover. This is defined in mathlib using filters. The main property of a compact set is IsCompact.elim_finite_subcover.
• IsClopen: a set that is both open and closed.
• IsIrreducible: a nonempty set that has contains no non-trivial pair of disjoint opens. See also the section below in the module doc.

For each of these definitions (except for IsClopen), we also have a class stating that the whole space satisfies that property: CompactSpace, PreirreducibleSpace, IrreducibleSpace.

Furthermore, we have four more classes:

• WeaklyLocallyCompactSpace: every point x has a compact neighborhood.
• LocallyCompactSpace: for every point x, every open neighborhood of x contains a compact neighborhood of x. The definition is formulated in terms of the neighborhood filter.
• SigmaCompactSpace: a space that is the union of a countably many compact subspaces;
• NoncompactSpace: a space that is not a compact space.

On the definition of irreducible and connected sets/spaces #

In informal mathematics, irreducible spaces are assumed to be nonempty. We formalise the predicate without that assumption as IsPreirreducible. In other words, the only difference is whether the empty space counts as irreducible. There are good reasons to consider the empty space to be “too simple to be simple” See also https://ncatlab.org/nlab/show/too+simple+to+be+simple, and in particular https://ncatlab.org/nlab/show/too+simple+to+be+simple#relationship_to_biased_definitions.

def IsCompact {α : Type u} [] (s : Set α) :

A set s is compact if for every nontrivial filter f that contains s, there exists a ∈ s such that every set of f meets every neighborhood of a.

Instances For
theorem IsCompact.compl_mem_sets {α : Type u} [] {s : Set α} (hs : ) {f : } (hf : ∀ (a : α), a ss nhds a f) :
s f

The complement to a compact set belongs to a filter f if it belongs to each filter 𝓝 a ⊓ f, a ∈ s.

theorem IsCompact.compl_mem_sets_of_nhdsWithin {α : Type u} [] {s : Set α} (hs : ) {f : } (hf : ∀ (a : α), a st, t t f) :
s f

The complement to a compact set belongs to a filter f if each a ∈ s has a neighborhood t within s such that tᶜ belongs to f.

theorem IsCompact.induction_on {α : Type u} [] {s : Set α} (hs : ) {p : Set αProp} (he : p ) (hmono : s t : Set α⦄ → s tp tp s) (hunion : s t : Set α⦄ → p sp tp (s t)) (hnhds : ∀ (x : α), x st, t p t) :
p s

If p : Set α → Prop is stable under restriction and union, and each point x of a compact set s has a neighborhood t within s such that p t, then p s holds.

theorem IsCompact.inter_right {α : Type u} [] {s : Set α} {t : Set α} (hs : ) (ht : ) :

The intersection of a compact set and a closed set is a compact set.

theorem IsCompact.inter_left {α : Type u} [] {s : Set α} {t : Set α} (ht : ) (hs : ) :

The intersection of a closed set and a compact set is a compact set.

theorem IsCompact.diff {α : Type u} [] {s : Set α} {t : Set α} (hs : ) (ht : ) :
IsCompact (s \ t)

The set difference of a compact set and an open set is a compact set.

theorem IsCompact.of_isClosed_subset {α : Type u} [] {s : Set α} {t : Set α} (hs : ) (ht : ) (h : t s) :

A closed subset of a compact set is a compact set.

theorem IsCompact.image_of_continuousOn {α : Type u} {β : Type v} [] [] {s : Set α} {f : αβ} (hs : ) (hf : ) :
theorem IsCompact.image {α : Type u} {β : Type v} [] [] {s : Set α} {f : αβ} (hs : ) (hf : ) :
theorem IsCompact.adherence_nhdset {α : Type u} [] {s : Set α} {t : Set α} {f : } (hs : ) (hf₂ : ) (ht₁ : ) (ht₂ : ∀ (a : α), a sa t) :
t f
theorem isCompact_iff_ultrafilter_le_nhds {α : Type u} [] {s : Set α} :
∀ (f : ), a, a s f nhds a
theorem IsCompact.ultrafilter_le_nhds {α : Type u} [] {s : Set α} :
∀ (f : ), a, a s f nhds a

Alias of the forward direction of isCompact_iff_ultrafilter_le_nhds.

theorem IsCompact.elim_directed_cover {α : Type u} [] {s : Set α} {ι : Type v} [hι : ] (hs : ) (U : ιSet α) (hUo : ∀ (i : ι), IsOpen (U i)) (hsU : s ⋃ (i : ι), U i) (hdU : Directed (fun x x_1 => x x_1) U) :
i, s U i

For every open directed cover of a compact set, there exists a single element of the cover which itself includes the set.

theorem IsCompact.elim_finite_subcover {α : Type u} [] {s : Set α} {ι : Type v} (hs : ) (U : ιSet α) (hUo : ∀ (i : ι), IsOpen (U i)) (hsU : s ⋃ (i : ι), U i) :
t, s ⋃ (i : ι) (_ : i t), U i

For every open cover of a compact set, there exists a finite subcover.

theorem IsCompact.elim_nhds_subcover' {α : Type u} [] {s : Set α} (hs : ) (U : (x : α) → x sSet α) (hU : ∀ (x : α) (hx : x s), U x hx nhds x) :
t, s ⋃ (x : s) (_ : x t), U x (_ : x s)
theorem IsCompact.elim_nhds_subcover {α : Type u} [] {s : Set α} (hs : ) (U : αSet α) (hU : ∀ (x : α), x sU x nhds x) :
t, (∀ (x : α), x tx s) s ⋃ (x : α) (_ : x t), U x
theorem IsCompact.disjoint_nhdsSet_left {α : Type u} [] {s : Set α} {l : } (hs : ) :
Disjoint () l ∀ (x : α), x sDisjoint (nhds x) l

The neighborhood filter of a compact set is disjoint with a filter l if and only if the neighborhood filter of each point of this set is disjoint with l.

theorem IsCompact.disjoint_nhdsSet_right {α : Type u} [] {s : Set α} {l : } (hs : ) :
Disjoint l () ∀ (x : α), x sDisjoint l (nhds x)

A filter l is disjoint with the neighborhood filter of a compact set if and only if it is disjoint with the neighborhood filter of each point of this set.

theorem IsCompact.elim_directed_family_closed {α : Type u} [] {s : Set α} {ι : Type v} [hι : ] (hs : ) (Z : ιSet α) (hZc : ∀ (i : ι), IsClosed (Z i)) (hsZ : s ⋂ (i : ι), Z i = ) (hdZ : Directed (fun x x_1 => x x_1) Z) :
i, s Z i =

For every directed family of closed sets whose intersection avoids a compact set, there exists a single element of the family which itself avoids this compact set.

theorem IsCompact.elim_finite_subfamily_closed {α : Type u} [] {s : Set α} {ι : Type v} (hs : ) (Z : ιSet α) (hZc : ∀ (i : ι), IsClosed (Z i)) (hsZ : s ⋂ (i : ι), Z i = ) :
t, s ⋂ (i : ι) (_ : i t), Z i =

For every family of closed sets whose intersection avoids a compact set, there exists a finite subfamily whose intersection avoids this compact set.

theorem LocallyFinite.finite_nonempty_inter_compact {α : Type u} [] {ι : Type u_3} {f : ιSet α} (hf : ) {s : Set α} (hs : ) :

If s is a compact set in a topological space α and f : ι → Set α is a locally finite family of sets, then f i ∩ s is nonempty only for a finitely many i.

theorem IsCompact.inter_iInter_nonempty {α : Type u} [] {s : Set α} {ι : Type v} (hs : ) (Z : ιSet α) (hZc : ∀ (i : ι), IsClosed (Z i)) (hsZ : ∀ (t : ), Set.Nonempty (s ⋂ (i : ι) (_ : i t), Z i)) :
Set.Nonempty (s ⋂ (i : ι), Z i)

To show that a compact set intersects the intersection of a family of closed sets, it is sufficient to show that it intersects every finite subfamily.

theorem IsCompact.nonempty_iInter_of_directed_nonempty_compact_closed {α : Type u} [] {ι : Type v} [hι : ] (Z : ιSet α) (hZd : Directed (fun x x_1 => x x_1) Z) (hZn : ∀ (i : ι), Set.Nonempty (Z i)) (hZc : ∀ (i : ι), IsCompact (Z i)) (hZcl : ∀ (i : ι), IsClosed (Z i)) :
Set.Nonempty (⋂ (i : ι), Z i)

Cantor's intersection theorem: the intersection of a directed family of nonempty compact closed sets is nonempty.

theorem IsCompact.nonempty_iInter_of_sequence_nonempty_compact_closed {α : Type u} [] (Z : Set α) (hZd : ∀ (i : ), Z (i + 1) Z i) (hZn : ∀ (i : ), Set.Nonempty (Z i)) (hZ0 : IsCompact (Z 0)) (hZcl : ∀ (i : ), IsClosed (Z i)) :
Set.Nonempty (⋂ (i : ), Z i)

Cantor's intersection theorem for sequences indexed by ℕ: the intersection of a decreasing sequence of nonempty compact closed sets is nonempty.

theorem IsCompact.elim_finite_subcover_image {α : Type u} {ι : Type u_1} [] {s : Set α} {b : Set ι} {c : ιSet α} (hs : ) (hc₁ : ∀ (i : ι), i bIsOpen (c i)) (hc₂ : s ⋃ (i : ι) (_ : i b), c i) :
b', b' b s ⋃ (i : ι) (_ : i b'), c i

For every open cover of a compact set, there exists a finite subcover.

theorem isCompact_of_finite_subcover {α : Type u} [] {s : Set α} (h : ∀ {ι : Type u} (U : ιSet α), (∀ (i : ι), IsOpen (U i)) → s ⋃ (i : ι), U it, s ⋃ (i : ι) (_ : i t), U i) :

A set s is compact if for every open cover of s, there exists a finite subcover.

theorem isCompact_of_finite_subfamily_closed {α : Type u} [] {s : Set α} (h : ∀ {ι : Type u} (Z : ιSet α), (∀ (i : ι), IsClosed (Z i)) → s ⋂ (i : ι), Z i = t, s ⋂ (i : ι) (_ : i t), Z i = ) :

A set s is compact if for every family of closed sets whose intersection avoids s, there exists a finite subfamily whose intersection avoids s.

theorem isCompact_iff_finite_subcover {α : Type u} [] {s : Set α} :
∀ {ι : Type u} (U : ιSet α), (∀ (i : ι), IsOpen (U i)) → s ⋃ (i : ι), U it, s ⋃ (i : ι) (_ : i t), U i

A set s is compact if and only if for every open cover of s, there exists a finite subcover.

theorem isCompact_iff_finite_subfamily_closed {α : Type u} [] {s : Set α} :
∀ {ι : Type u} (Z : ιSet α), (∀ (i : ι), IsClosed (Z i)) → s ⋂ (i : ι), Z i = t, s ⋂ (i : ι) (_ : i t), Z i =

A set s is compact if and only if for every family of closed sets whose intersection avoids s, there exists a finite subfamily whose intersection avoids s.

theorem IsCompact.mem_nhdsSet_prod_of_forall {α : Type u} {β : Type v} [] {K : Set α} {l : } {s : Set (α × β)} (hK : ) (hs : ∀ (x : α), x Ks nhds x ×ˢ l) :
s ×ˢ l

If s : Set (α × β) belongs to 𝓝 x ×ˢ l for all x from a compact set K, then it belongs to (𝓝ˢ K) ×ˢ l, i.e., there exist an open U ⊇ K and t ∈ l such that U ×ˢ t ⊆ s.

theorem IsCompact.nhdsSet_prod_eq_biSup {α : Type u} {β : Type v} [] {K : Set α} (hK : ) (l : ) :
×ˢ l = ⨆ (x : α) (_ : x K), nhds x ×ˢ l
theorem IsCompact.prod_nhdsSet_eq_biSup {α : Type u} {β : Type v} [] {K : Set β} (hK : ) (l : ) :
l ×ˢ = ⨆ (y : β) (_ : y K), l ×ˢ nhds y
theorem IsCompact.mem_prod_nhdsSet_of_forall {α : Type u} {β : Type v} [] {K : Set β} {l : } {s : Set (α × β)} (hK : ) (hs : ∀ (y : β), y Ks l ×ˢ nhds y) :
s l ×ˢ

If s : Set (α × β) belongs to l ×ˢ 𝓝 y for all y from a compact set K, then it belongs to l ×ˢ (𝓝ˢ K), i.e., there exist t ∈ l and an open U ⊇ K such that t ×ˢ U ⊆ s.

theorem IsCompact.eventually_forall_of_forall_eventually {α : Type u} {β : Type v} [] [] {x₀ : α} {K : Set β} (hK : ) {P : αβProp} (hP : ∀ (y : β), y K∀ᶠ (z : α × β) in nhds (x₀, y), P z.fst z.snd) :
∀ᶠ (x : α) in nhds x₀, (y : β) → y KP x y

To show that ∀ y ∈ K, P x y holds for x close enough to x₀ when K is compact, it is sufficient to show that for all y₀ ∈ K there P x y holds for (x, y) close enough to (x₀, y₀).

Provided for backwards compatibility, see IsCompact.mem_prod_nhdsSet_of_forall for a stronger statement.

@[simp]
theorem isCompact_empty {α : Type u} [] :
@[simp]
theorem isCompact_singleton {α : Type u} [] {a : α} :
theorem Set.Subsingleton.isCompact {α : Type u} [] {s : Set α} (hs : ) :
theorem Set.Finite.isCompact_biUnion {α : Type u} {ι : Type u_1} [] {s : Set ι} {f : ιSet α} (hs : ) (hf : ∀ (i : ι), i sIsCompact (f i)) :
IsCompact (⋃ (i : ι) (_ : i s), f i)
theorem Finset.isCompact_biUnion {α : Type u} {ι : Type u_1} [] (s : ) {f : ιSet α} (hf : ∀ (i : ι), i sIsCompact (f i)) :
IsCompact (⋃ (i : ι) (_ : i s), f i)
theorem isCompact_accumulate {α : Type u} [] {K : Set α} (hK : ∀ (n : ), IsCompact (K n)) (n : ) :
theorem Set.Finite.isCompact_sUnion {α : Type u} [] {S : Set (Set α)} (hf : ) (hc : ∀ (s : Set α), s S) :
theorem isCompact_iUnion {α : Type u} [] {ι : Sort u_3} {f : ιSet α} [] (h : ∀ (i : ι), IsCompact (f i)) :
IsCompact (⋃ (i : ι), f i)
theorem Set.Finite.isCompact {α : Type u} [] {s : Set α} (hs : ) :
theorem IsCompact.finite_of_discrete {α : Type u} [] [] {s : Set α} (hs : ) :
theorem isCompact_iff_finite {α : Type u} [] [] {s : Set α} :
theorem IsCompact.union {α : Type u} [] {s : Set α} {t : Set α} (hs : ) (ht : ) :
theorem IsCompact.insert {α : Type u} [] {s : Set α} (hs : ) (a : α) :
theorem exists_subset_nhds_of_isCompact' {α : Type u} [] {ι : Type u_3} [] {V : ιSet α} (hV : Directed (fun x x_1 => x x_1) V) (hV_cpct : ∀ (i : ι), IsCompact (V i)) (hV_closed : ∀ (i : ι), IsClosed (V i)) {U : Set α} (hU : ∀ (x : α), x ⋂ (i : ι), V iU nhds x) :
i, V i U

If V : ι → Set α is a decreasing family of closed compact sets then any neighborhood of ⋂ i, V i contains some V i. We assume each V i is compact and closed because α is not assumed to be Hausdorff. See exists_subset_nhd_of_compact for version assuming this.

theorem isCompact_open_iff_eq_finite_iUnion_of_isTopologicalBasis {α : Type u} {ι : Type u_1} [] (b : ιSet α) (hb : ) (hb' : ∀ (i : ι), IsCompact (b i)) (U : Set α) :
s, U = ⋃ (i : ι) (_ : 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

def Filter.cocompact (α : Type u_3) [] :

Filter.cocompact is the filter generated by complements to compact sets.

Instances For
theorem Filter.hasBasis_cocompact {α : Type u} [] :
Filter.HasBasis () IsCompact compl
theorem Filter.mem_cocompact {α : Type u} [] {s : Set α} :
t, t s
theorem Filter.mem_cocompact' {α : Type u} [] {s : Set α} :
t, s t
theorem IsCompact.compl_mem_cocompact {α : Type u} [] {s : Set α} (hs : ) :
theorem Filter.cocompact_le_cofinite {α : Type u} [] :
Filter.cofinite
theorem Filter.cocompact_eq_cofinite (α : Type u_3) [] [] :
= Filter.cofinite
@[simp]
theorem Nat.cocompact_eq :
= Filter.atTop
theorem Filter.Tendsto.isCompact_insert_range_of_cocompact {α : Type u} {β : Type v} [] [] {f : αβ} {b : β} (hf : Filter.Tendsto f () (nhds b)) (hfc : ) :
theorem Filter.Tendsto.isCompact_insert_range_of_cofinite {α : Type u} {ι : Type u_1} [] {f : ια} {a : α} (hf : Filter.Tendsto f Filter.cofinite (nhds a)) :
theorem Filter.Tendsto.isCompact_insert_range {α : Type u} [] {f : α} {a : α} (hf : Filter.Tendsto f Filter.atTop (nhds a)) :
def Filter.coclosedCompact (α : Type u_3) [] :

Filter.coclosedCompact is the filter generated by complements to closed compact sets. In a Hausdorff space, this is the same as Filter.cocompact.

Instances For
theorem Filter.hasBasis_coclosedCompact {α : Type u} [] :
Filter.HasBasis () (fun s => ) compl
theorem Filter.mem_coclosedCompact {α : Type u} [] {s : Set α} :
t, t s
theorem Filter.mem_coclosed_compact' {α : Type u} [] {s : Set α} :
t, s t
theorem IsCompact.compl_mem_coclosedCompact_of_isClosed {α : Type u} [] {s : Set α} (hs : ) (hs' : ) :
def Bornology.inCompact (α : Type u) [] :

Sets that are contained in a compact set form a bornology. Its cobounded filter is Filter.cocompact. See also Bornology.relativelyCompact the bornology of sets with compact closure.

Instances For
theorem Bornology.inCompact.isBounded_iff {α : Type u} [] {s : Set α} :
t, s t
theorem IsCompact.nhdsSet_prod_eq {α : Type u} {β : Type v} [] [] {s : Set α} {t : Set β} (hs : ) (ht : ) :

If s and t are compact sets, then the set neighborhoods filter of s ×ˢ t is the product of set neighborhoods filters for s and t.

For general sets, only the ≤ inequality holds, see nhdsSet_prod_le.

theorem nhdsSet_prod_le {α : Type u} {β : Type v} [] [] (s : Set α) (t : Set β) :

The product of a neighborhood of s and a neighborhood of t is a neighborhood of s ×ˢ t, formulated in terms of a filter inequality.

theorem generalized_tube_lemma {α : Type u} {β : Type v} [] [] {s : Set α} (hs : ) {t : Set β} (ht : ) {n : Set (α × β)} (hn : ) (hp : s ×ˢ t n) :
u v, s u t v u ×ˢ v n

If s and t are compact sets and n is an open neighborhood of s × t, then there exist open neighborhoods u ⊇ s and v ⊇ t such that u × v ⊆ n.

See also IsCompact.nhdsSet_prod_eq.

class CompactSpace (α : Type u_3) [] :
• isCompact_univ : IsCompact Set.univ

In a compact space, Set.univ is a compact set.

Type class for compact spaces. Separation is sometimes included in the definition, especially in the French literature, but we do not include it here.

Instances
instance Subsingleton.compactSpace {α : Type u} [] [] :
theorem isCompact_univ_iff {α : Type u} [] :
IsCompact Set.univ
theorem isCompact_univ {α : Type u} [] [h : ] :
IsCompact Set.univ
theorem cluster_point_of_compact {α : Type u} [] [] (f : ) [] :
x,
theorem CompactSpace.elim_nhds_subcover {α : Type u} [] [] (U : αSet α) (hU : ∀ (x : α), U x nhds x) :
t, ⋃ (x : α) (_ : x t), U x =
theorem compactSpace_of_finite_subfamily_closed {α : Type u} [] (h : ∀ {ι : Type u} (Z : ιSet α), (∀ (i : ι), IsClosed (Z i)) → ⋂ (i : ι), Z i = t, ⋂ (i : ι) (_ : i t), Z i = ) :
theorem IsClosed.isCompact {α : Type u} [] [] {s : Set α} (h : ) :
class NoncompactSpace (α : Type u_3) [] :
• noncompact_univ : ¬IsCompact Set.univ

In a noncompact space, Set.univ is not a compact set.

α is a noncompact topological space if it is not a compact space.

Instances
theorem noncompact_univ (α : Type u_3) [] [] :
¬IsCompact Set.univ
theorem IsCompact.ne_univ {α : Type u} [] [] {s : Set α} (hs : ) :
s Set.univ
instance instNeBotCocompact {α : Type u} [] [] :
@[simp]
theorem Filter.cocompact_eq_bot {α : Type u} [] [] :
instance instNeBotCoclosedCompact {α : Type u} [] [] :
theorem noncompactSpace_of_neBot {α : Type u} [] :
theorem not_compactSpace_iff {α : Type u} [] :
theorem finite_of_compact_of_discrete {α : Type u} [] [] [] :

A compact discrete space is finite.

theorem exists_nhds_ne_neBot (α : Type u_3) [] [] [] :
theorem finite_cover_nhds_interior {α : Type u} [] [] {U : αSet α} (hU : ∀ (x : α), U x nhds x) :
t, ⋃ (x : α) (_ : x t), interior (U x) = Set.univ
theorem finite_cover_nhds {α : Type u} [] [] {U : αSet α} (hU : ∀ (x : α), U x nhds x) :
t, ⋃ (x : α) (_ : x t), U x = Set.univ
theorem LocallyFinite.finite_nonempty_of_compact {α : Type u} [] {ι : Type u_3} [] {f : ιSet α} (hf : ) :

If α is a compact space, then a locally finite family of sets of α can have only finitely many nonempty elements.

theorem LocallyFinite.finite_of_compact {α : Type u} [] {ι : Type u_3} [] {f : ιSet α} (hf : ) (hne : ∀ (i : ι), Set.Nonempty (f i)) :
Set.Finite Set.univ

If α is a compact space, then a locally finite family of nonempty sets of α can have only finitely many elements, Set.Finite version.

noncomputable def LocallyFinite.fintypeOfCompact {α : Type u} [] {ι : Type u_3} [] {f : ιSet α} (hf : ) (hne : ∀ (i : ι), Set.Nonempty (f i)) :

If α is a compact space, then a locally finite family of nonempty sets of α can have only finitely many elements, Fintype version.

Instances For
theorem Filter.comap_cocompact_le {α : Type u} {β : Type v} [] [] {f : αβ} (hf : ) :

The comap of the cocompact filter on β by a continuous function f : α → β is less than or equal to the cocompact filter on α. This is a reformulation of the fact that images of compact sets are compact.

theorem isCompact_range {α : Type u} {β : Type v} [] [] [] {f : αβ} (hf : ) :
theorem isCompact_diagonal {α : Type u} [] [] :
theorem isClosedMap_snd_of_compactSpace {X : Type u_3} [] [] {Y : Type u_4} [] :
IsClosedMap Prod.snd

If X is a compact topological space, then Prod.snd : X × Y → Y is a closed map.

theorem exists_subset_nhds_of_compactSpace {α : Type u} [] [] {ι : Type u_3} [] {V : ιSet α} (hV : Directed (fun x x_1 => x x_1) V) (hV_closed : ∀ (i : ι), IsClosed (V i)) {U : Set α} (hU : ∀ (x : α), x ⋂ (i : ι), V iU nhds x) :
i, V i U
theorem Inducing.isCompact_iff {α : Type u} {β : Type v} [] [] {f : αβ} (hf : ) {s : Set α} :

If f : α → β is an Inducing map, the image f '' s of a set s is compact if and only if s is compact.

theorem Embedding.isCompact_iff_isCompact_image {α : Type u} {β : Type v} [] [] {s : Set α} {f : αβ} (hf : ) :

If f : α → β is an Embedding (or more generally, an Inducing map, see Inducing.isCompact_iff), the image f '' s of a set s is compact if and only if the set s is compact.

theorem ClosedEmbedding.isCompact_preimage {α : Type u} {β : Type v} [] [] {f : αβ} (hf : ) {K : Set β} (hK : ) :

The preimage of a compact set under a closed embedding is a compact set.

theorem ClosedEmbedding.tendsto_cocompact {α : Type u} {β : Type v} [] [] {f : αβ} (hf : ) :

A closed embedding is proper, ie, inverse images of compact sets are contained in compacts. Moreover, the preimage of a compact set is compact, see ClosedEmbedding.isCompact_preimage.

theorem isCompact_iff_isCompact_in_subtype {α : Type u} [] {p : αProp} {s : Set { a // p a }} :
IsCompact (Subtype.val '' s)
theorem isCompact_iff_isCompact_univ {α : Type u} [] {s : Set α} :
IsCompact Set.univ
theorem isCompact_iff_compactSpace {α : Type u} [] {s : Set α} :
theorem IsCompact.finite {α : Type u} [] {s : Set α} (hs : ) (hs' : ) :
theorem exists_nhds_ne_inf_principal_neBot {α : Type u} [] {s : Set α} (hs : ) (hs' : ) :
z, z s Filter.NeBot (nhdsWithin z {z} )
theorem ClosedEmbedding.noncompactSpace {α : Type u} {β : Type v} [] [] [] {f : αβ} (hf : ) :
theorem ClosedEmbedding.compactSpace {α : Type u} {β : Type v} [] [] [h : ] {f : αβ} (hf : ) :
theorem IsCompact.prod {α : Type u} {β : Type v} [] [] {s : Set α} {t : Set β} (hs : ) (ht : ) :
instance Finite.compactSpace {α : Type u} [] [] :

Finite topological spaces are compact.

instance instCompactSpaceProdInstTopologicalSpaceProd {α : Type u} {β : Type v} [] [] [] [] :

The product of two compact spaces is compact.

instance instCompactSpaceSumInstTopologicalSpaceSum {α : Type u} {β : Type v} [] [] [] [] :

The disjoint union of two compact spaces is compact.

instance instCompactSpaceSigmaInstTopologicalSpaceSigma {ι : Type u_1} {π : ιType u_2} [] [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), CompactSpace (π i)] :
CompactSpace ((i : ι) × π i)
theorem Filter.coprod_cocompact {α : Type u} {β : Type v} [] [] :

The coproduct of the cocompact filters on two topological spaces is the cocompact filter on their product.

theorem Prod.noncompactSpace_iff {α : Type u} {β : Type v} [] [] :
instance Prod.noncompactSpace_left {α : Type u} {β : Type v} [] [] [] [] :
instance Prod.noncompactSpace_right {α : Type u} {β : Type v} [] [] [] [] :
theorem isCompact_pi_infinite {ι : Type u_1} {π : ιType u_2} [(i : ι) → TopologicalSpace (π i)] {s : (i : ι) → Set (π i)} :
(∀ (i : ι), IsCompact (s i)) → IsCompact {x | ∀ (i : ι), x i s i}

Tychonoff's theorem: product of compact sets is compact.

theorem isCompact_univ_pi {ι : Type u_1} {π : ιType u_2} [(i : ι) → TopologicalSpace (π i)] {s : (i : ι) → Set (π i)} (h : ∀ (i : ι), IsCompact (s i)) :
IsCompact (Set.pi Set.univ s)

Tychonoff's theorem formulated using Set.pi: product of compact sets is compact.

instance Pi.compactSpace {ι : Type u_1} {π : ιType u_2} [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), CompactSpace (π i)] :
CompactSpace ((i : ι) → π i)
instance Function.compactSpace {β : Type v} {ι : Type u_1} [] [] :
CompactSpace (ιβ)
theorem Filter.coprodᵢ_cocompact {δ : Type u_3} {κ : δType u_4} [(d : δ) → TopologicalSpace (κ d)] :
(Filter.coprodᵢ fun d => Filter.cocompact (κ d)) = Filter.cocompact ((d : δ) → κ d)

Tychonoff's theorem formulated in terms of filters: Filter.cocompact on an indexed product type Π d, κ d the Filter.coprodᵢ of filters Filter.cocompact on κ d.

instance Quot.compactSpace {α : Type u} [] {r : ααProp} [] :
instance Quotient.compactSpace {α : Type u} [] {s : } [] :
class WeaklyLocallyCompactSpace (α : Type u_3) [] :
• exists_compact_mem_nhds : ∀ (x : α), s, s nhds x

Every point of a weakly locally compact space admits a compact neighborhood.

We say that a topological space is a weakly locally compact space, if each point of this space admits a compact neighborhood.

Instances
instance instWeaklyLocallyCompactSpaceForAllTopologicalSpace {ι : Type u_3} [] {X : ιType u_4} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), ] :
WeaklyLocallyCompactSpace ((i : ι) → X i)
instance instWeaklyLocallyCompactSpace {α : Type u} [] [] :
theorem exists_compact_superset {α : Type u} [] {K : Set α} (hK : ) :
K', K interior K'

In a weakly locally compact space, every compact set is contained in the interior of a compact set.

theorem disjoint_nhds_cocompact {α : Type u} [] (x : α) :
Disjoint (nhds x) ()

In a weakly locally compact space, the filters 𝓝 x and cocompact α are disjoint for all α.

class LocallyCompactSpace (α : Type u_3) [] :
• local_compact_nhds : ∀ (x : α) (n : Set α), n nhds xs, s nhds x s n

In a locally compact space, every neighbourhood of every point contains a compact neighbourhood of that same point.

There are various definitions of "locally compact space" in the literature, which agree for Hausdorff spaces but not in general. This one is the precise condition on X needed for the evaluation map C(X, Y) × X → Y to be continuous for all Y when C(X, Y) is given the compact-open topology.

See also WeaklyLocallyCompactSpace, a typeclass that only assumes that each point has a compact neighborhood.

Instances
theorem compact_basis_nhds {α : Type u} [] (x : α) :
Filter.HasBasis (nhds x) (fun s => s nhds x ) fun s => s
theorem local_compact_nhds {α : Type u} [] {x : α} {n : Set α} (h : n nhds x) :
s, s nhds x s n
theorem locallyCompactSpace_of_hasBasis {α : Type u} [] {ι : αType u_3} {p : (x : α) → ι xProp} {s : (x : α) → ι xSet α} (h : ∀ (x : α), Filter.HasBasis (nhds x) (p x) (s x)) (hc : ∀ (x : α) (i : ι x), p x iIsCompact (s x i)) :
instance Prod.locallyCompactSpace (α : Type u_3) (β : Type u_4) [] [] :
instance Pi.locallyCompactSpace_of_finite {ι : Type u_1} {π : ιType u_2} [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), LocallyCompactSpace (π i)] [] :
LocallyCompactSpace ((i : ι) → π i)

In general it suffices that all but finitely many of the spaces are compact, but that's not straightforward to state and use.

instance Pi.locallyCompactSpace {ι : Type u_1} {π : ιType u_2} [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), LocallyCompactSpace (π i)] [∀ (i : ι), CompactSpace (π i)] :
LocallyCompactSpace ((i : ι) → π i)

For spaces that are not Hausdorff.

instance Function.locallyCompactSpace_of_finite {β : Type v} {ι : Type u_1} [] [] :
instance Function.locallyCompactSpace {β : Type v} {ι : Type u_1} [] [] :
theorem exists_compact_subset {α : Type u} [] {x : α} {U : Set α} (hU : ) (hx : x U) :
K, x K U

A reformulation of the definition of locally compact space: In a locally compact space, every open set containing x has a compact subset containing x in its interior.

theorem exists_compact_between {α : Type u} [] [hα : ] {K : Set α} {U : Set α} (hK : ) (hU : ) (h_KU : K U) :
L, K L U

In a locally compact space, for every containment K ⊆ U of a compact set K in an open set U, there is a compact neighborhood L such that K ⊆ L ⊆ U: equivalently, there is a compact L such that K ⊆ interior L and L ⊆ U.

theorem ClosedEmbedding.locallyCompactSpace {α : Type u} {β : Type v} [] [] {f : αβ} (hf : ) :
theorem IsClosed.locallyCompactSpace {α : Type u} [] {s : Set α} (hs : ) :
theorem OpenEmbedding.locallyCompactSpace {α : Type u} {β : Type v} [] [] {f : αβ} (hf : ) :
theorem IsOpen.locallyCompactSpace {α : Type u} [] {s : Set α} (hs : ) :
theorem Ultrafilter.le_nhds_lim {α : Type u} [] [] (F : ) :
F
theorem IsClosed.exists_minimal_nonempty_closed_subset {α : Type u} [] [] {S : Set α} (hS : ) (hne : ) :
V, V S ∀ (V' : Set α), V' VIsClosed V'V' = V
class SigmaCompactSpace (α : Type u_3) [] :
• exists_compact_covering : K, (∀ (n : ), IsCompact (K n)) ⋃ (n : ), K n = Set.univ

In a σ-compact space, there exists (by definition) a countable collection of compact subspaces that cover the entire space.

A σ-compact space is a space that is the union of a countable collection of compact subspaces. Note that a locally compact separable T₂ space need not be σ-compact. The sequence can be extracted using compactCovering.

Instances
instance CompactSpace.sigma_compact {α : Type u} [] [] :
theorem SigmaCompactSpace.of_countable {α : Type u} [] (S : Set (Set α)) (Hc : ) (Hcomp : ∀ (s : Set α), s S) (HU : ⋃₀ S = Set.univ) :
def compactCovering (α : Type u) [] :
Set α

A choice of compact covering for a σ-compact space, chosen to be monotone.

Instances For
theorem isCompact_compactCovering (α : Type u) [] (n : ) :
theorem iUnion_compactCovering (α : Type u) [] :
⋃ (n : ), = Set.univ
theorem compactCovering_subset (α : Type u) [] ⦃m : ⦃n : (h : m n) :
theorem exists_mem_compactCovering {α : Type u} [] (x : α) :
n, x
instance instSigmaCompactSpaceForAllTopologicalSpace {ι : Type u_1} {π : ιType u_2} [] [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), SigmaCompactSpace (π i)] :
SigmaCompactSpace ((i : ι) → π i)
instance instSigmaCompactSpaceSigmaInstTopologicalSpaceSigma {ι : Type u_1} {π : ιType u_2} [] [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), SigmaCompactSpace (π i)] :
SigmaCompactSpace ((i : ι) × π i)
theorem ClosedEmbedding.sigmaCompactSpace {α : Type u} {β : Type v} [] [] {e : βα} (he : ) :
theorem IsClosed.sigmaCompactSpace {α : Type u} [] {s : Set α} (hs : ) :
theorem LocallyFinite.countable_univ {α : Type u} [] {ι : Type u_3} {f : ιSet α} (hf : ) (hne : ∀ (i : ι), Set.Nonempty (f i)) :
Set.Countable Set.univ

If α is a σ-compact space, then a locally finite family of nonempty sets of α can have only countably many elements, Set.Countable version.

noncomputable def LocallyFinite.encodable {α : Type u} [] {ι : Type u_3} {f : ιSet α} (hf : ) (hne : ∀ (i : ι), Set.Nonempty (f i)) :

If f : ι → Set α is a locally finite covering of a σ-compact topological space by nonempty sets, then the index type ι is encodable.

Instances For
theorem countable_cover_nhdsWithin_of_sigma_compact {α : Type u} [] {f : αSet α} {s : Set α} (hs : ) (hf : ∀ (x : α), x sf x ) :
t x, s ⋃ (x : α) (_ : x t), f x

In a topological space with sigma compact topology, if f is a function that sends each point x of a closed set s to a neighborhood of x within s, then for some countable set t ⊆ s, the neighborhoods f x, x ∈ t, cover the whole set s.

theorem countable_cover_nhds_of_sigma_compact {α : Type u} [] {f : αSet α} (hf : ∀ (x : α), f x nhds x) :
s, ⋃ (x : α) (_ : x s), f x = Set.univ

In a topological space with sigma compact topology, if f is a function that sends each point x to a neighborhood of x, then for some countable set s, the neighborhoods f x, x ∈ s, cover the whole space.

structure CompactExhaustion (X : Type u_3) [] :
Type u_3
• toFun : Set X

The sequence of compact sets that form a compact exhaustion.

• isCompact' : ∀ (n : ),

The sets in the compact exhaustion are in fact compact.

• subset_interior_succ' : ∀ (n : ), interior (CompactExhaustion.toFun s (n + 1))

The sets in the compact exhaustion form a sequence: each set is contained in the interior of the next.

• iUnion_eq' : ⋃ (n : ), = Set.univ

The union of all sets in a compact exhaustion equals the entire space.

An exhaustion by compact sets of a topological space is a sequence of compact sets K n such that K n ⊆ interior (K (n + 1)) and ⋃ n, K n = univ.

If X is a locally compact sigma compact space, then CompactExhaustion.choice X provides a choice of an exhaustion by compact sets. This choice is also available as (default : CompactExhaustion X).

Instances For
@[simp]
theorem CompactExhaustion.toFun_eq_coe {α : Type u} [] (K : ) :
K.toFun = K
theorem CompactExhaustion.isCompact {α : Type u} [] (K : ) (n : ) :
IsCompact (K n)
theorem CompactExhaustion.subset_interior_succ {α : Type u} [] (K : ) (n : ) :
K n interior (K (n + 1))
theorem CompactExhaustion.subset {α : Type u} [] (K : ) ⦃m : ⦃n : (h : m n) :
K m K n
theorem CompactExhaustion.subset_succ {α : Type u} [] (K : ) (n : ) :
K n K (n + 1)
theorem CompactExhaustion.subset_interior {α : Type u} [] (K : ) ⦃m : ⦃n : (h : m < n) :
K m interior (K n)
theorem CompactExhaustion.iUnion_eq {α : Type u} [] (K : ) :
⋃ (n : ), K n = Set.univ
theorem CompactExhaustion.exists_mem {α : Type u} [] (K : ) (x : α) :
n, x K n
noncomputable def CompactExhaustion.find {α : Type u} [] (K : ) (x : α) :

The minimal n such that x ∈ K n.

Instances For
theorem CompactExhaustion.mem_find {α : Type u} [] (K : ) (x : α) :
x K ()
theorem CompactExhaustion.mem_iff_find_le {α : Type u} [] (K : ) {x : α} {n : } :
x K n
def CompactExhaustion.shiftr {α : Type u} [] (K : ) :

Prepend the empty set to a compact exhaustion K n.

Instances For
@[simp]
theorem CompactExhaustion.find_shiftr {α : Type u} [] (K : ) (x : α) :
theorem CompactExhaustion.mem_diff_shiftr_find {α : Type u} [] (K : ) (x : α) :
x ↑() () \ ↑() ()
noncomputable def CompactExhaustion.choice (X : Type u_3) [] :

A choice of an exhaustion by compact sets of a weakly locally compact σ-compact space.

Instances For
def IsClopen {α : Type u} [] (s : Set α) :

A set is clopen if it is both open and closed.

Instances For
theorem IsClopen.isOpen {α : Type u} [] {s : Set α} (hs : ) :
theorem IsClopen.isClosed {α : Type u} [] {s : Set α} (hs : ) :
theorem isClopen_iff_frontier_eq_empty {α : Type u} [] {s : Set α} :
theorem IsClopen.frontier_eq {α : Type u} [] {s : Set α} :

Alias of the forward direction of isClopen_iff_frontier_eq_empty.

theorem IsClopen.union {α : Type u} [] {s : Set α} {t : Set α} (hs : ) (ht : ) :
theorem IsClopen.inter {α : Type u} [] {s : Set α} {t : Set α} (hs : ) (ht : ) :
@[simp]
theorem isClopen_empty {α : Type u} [] :
@[simp]
theorem isClopen_univ {α : Type u} [] :
IsClopen Set.univ
theorem IsClopen.compl {α : Type u} [] {s : Set α} (hs : ) :
@[simp]
theorem isClopen_compl_iff {α : Type u} [] {s : Set α} :
theorem IsClopen.diff {α : Type u} [] {s : Set α} {t : Set α} (hs : ) (ht : ) :
IsClopen (s \ t)
theorem IsClopen.prod {α : Type u} {β : Type v} [] [] {s : Set α} {t : Set β} (hs : ) (ht : ) :
theorem isClopen_iUnion_of_finite {α : Type u} [] {β : Type u_3} [] {s : βSet α} (h : ∀ (i : β), IsClopen (s i)) :
IsClopen (⋃ (i : β), s i)
theorem Set.Finite.isClopen_biUnion {α : Type u} [] {β : Type u_3} {s : Set β} {f : βSet α} (hs : ) (h : ∀ (i : β), i sIsClopen (f i)) :
IsClopen (⋃ (i : β) (_ : i s), f i)
theorem isClopen_biUnion_finset {α : Type u} [] {β : Type u_3} {s : } {f : βSet α} (h : ∀ (i : β), i sIsClopen (f i)) :
IsClopen (⋃ (i : β) (_ : i s), f i)
theorem isClopen_iInter_of_finite {α : Type u} [] {β : Type u_3} [] {s : βSet α} (h : ∀ (i : β), IsClopen (s i)) :
IsClopen (⋂ (i : β), s i)
theorem Set.Finite.isClopen_biInter {α : Type u} [] {β : Type u_3} {s : Set β} (hs : ) {f : βSet α} (h : ∀ (i : β), i sIsClopen (f i)) :
IsClopen (⋂ (i : β) (_ : i s), f i)
theorem isClopen_biInter_finset {α : Type u} [] {β : Type u_3} {s : } {f : βSet α} (h : ∀ (i : β), i sIsClopen (f i)) :
IsClopen (⋂ (i : β) (_ : i s), f i)
theorem IsClopen.preimage {α : Type u} {β : Type v} [] [] {s : Set β} (h : ) {f : αβ} (hf : ) :
theorem ContinuousOn.preimage_clopen_of_clopen {α : Type u} {β : Type v} [] [] {f : αβ} {s : Set α} {t : Set β} (hf : ) (hs : ) (ht : ) :
theorem isClopen_inter_of_disjoint_cover_clopen {α : Type u} [] {Z : Set α} {a : Set α} {b : Set α} (h : ) (cover : Z a b) (ha : ) (hb : ) (hab : Disjoint a b) :

The intersection of a disjoint covering by two open sets of a clopen set will be clopen.

@[simp]
theorem isClopen_discrete {α : Type u} [] [] (x : Set α) :
theorem isClopen_range_inl {α : Type u} {β : Type v} [] [] :
theorem isClopen_range_inr {α : Type u} {β : Type v} [] [] :
theorem isClopen_range_sigmaMk {ι : Type u_3} {σ : ιType u_4} [(i : ι) → TopologicalSpace (σ i)] {i : ι} :
theorem QuotientMap.isClopen_preimage {α : Type u} {β : Type v} [] [] {f : αβ} (hf : ) {s : Set β} :
theorem continuous_boolIndicator_iff_clopen {X : Type u_3} [] (U : Set X) :
theorem continuousOn_boolIndicator_iff_clopen {X : Type u_3} [] (s : Set X) (U : Set X) :
IsClopen (Subtype.val ⁻¹' U)
def IsPreirreducible {α : Type u} [] (s : Set α) :

A preirreducible set s is one where there is no non-trivial pair of disjoint opens on s.

Instances For
def IsIrreducible {α : Type u} [] (s : Set α) :

An irreducible set s is one that is nonempty and where there is no non-trivial pair of disjoint opens on s.

Instances For
theorem IsIrreducible.nonempty {α : Type u} [] {s : Set α} (h : ) :
theorem IsIrreducible.isPreirreducible {α : Type u} [] {s : Set α} (h : ) :
theorem isPreirreducible_empty {α : Type u} [] :
theorem Set.Subsingleton.isPreirreducible {α : Type u} [] {s : Set α} (hs : ) :
theorem isPreirreducible_singleton {α : Type u} [] {x : α} :
theorem isIrreducible_singleton {α : Type u} [] {x : α} :
theorem isPreirreducible_iff_closure {α : Type u} [] {s : Set α} :
theorem isIrreducible_iff_closure {α : Type u} [] {s : Set α} :
theorem IsPreirreducible.closure {α : Type u} [] {s : Set α} :

Alias of the reverse direction of isPreirreducible_iff_closure.

theorem IsIrreducible.closure {α : Type u} [] {s : Set α} :

Alias of the reverse direction of isIrreducible_iff_closure.

theorem exists_preirreducible {α : Type u} [] (s : Set α) (H : ) :
t, s t ∀ (u : Set α), t uu = t
def irreducibleComponents (α : Type u_3) [] :
Set (Set α)

The set of irreducible components of a topological space.

Instances For
theorem isClosed_of_mem_irreducibleComponents {α : Type u} [] (s : Set α) (H : ) :
theorem irreducibleComponents_eq_maximals_closed (α : Type u_3) [] :
= maximals (fun x x_1 => x x_1) {s | }
def irreducibleComponent {α : Type u} [] (x : α) :
Set α

A maximal irreducible set that contains a given point.

Instances For
theorem irreducibleComponent_property {α : Type u} [] (x : α) :
∀ (u : Set α),
theorem mem_irreducibleComponent {α : Type u} [] {x : α} :
theorem isIrreducible_irreducibleComponent {α : Type u} [] {x : α} :
theorem eq_irreducibleComponent {α : Type u} [] {x : α} {s : Set α} :
theorem isClosed_irreducibleComponent {α : Type u} [] {x : α} :
class PreirreducibleSpace (α : Type u) [] :
• isPreirreducible_univ : IsPreirreducible Set.univ

In a preirreducible space, Set.univ is a preirreducible set.

A preirreducible space is one where there is no non-trivial pair of disjoint opens.

Instances
class IrreducibleSpace (α : Type u) [] extends :

An irreducible space is one that is nonempty and where there is no non-trivial pair of disjoint opens.

Instances
theorem irreducibleSpace_def (α : Type u) [] :
theorem nonempty_preirreducible_inter {α : Type u} [] {s : Set α} {t : Set α} :
Set.Nonempty (s t)
theorem IsOpen.dense {α : Type u} [] {s : Set α} (ho : ) (hne : ) :

In a (pre)irreducible space, a nonempty open set is dense.

theorem IsPreirreducible.image {α : Type u} {β : Type v} [] [] {s : Set α} (H : ) (f : αβ) (hf : ) :
theorem IsIrreducible.image {α : Type u} {β : Type v} [] [] {s : Set α} (H : ) (f : αβ) (hf : ) :
theorem Subtype.preirreducibleSpace {α : Type u} [] {s : Set α} (h : ) :
theorem Subtype.irreducibleSpace {α : Type u} [] {s : Set α} (h : ) :

An infinite type with cofinite topology is an irreducible topological space.

theorem isIrreducible_iff_sInter {α : Type u} [] {s : Set α} :
∀ (U : Finset (Set α)), (∀ (u : Set α), u U) → (∀ (u : Set α), u USet.Nonempty (s u)) → Set.Nonempty (s ⋂₀ U)

A set s is irreducible if and only if for every finite collection of open sets all of whose members intersect s, s also intersects the intersection of the entire collection (i.e., there is an element of s contained in every member of the collection).

theorem isPreirreducible_iff_closed_union_closed {α : Type u} [] {s : Set α} :
∀ (z₁ z₂ : Set α), IsClosed z₁IsClosed z₂s z₁ z₂s z₁ s z₂

A set is preirreducible if and only if for every cover by two closed sets, it is contained in one of the two covering sets.

theorem isIrreducible_iff_sUnion_closed {α : Type u} [] {s : Set α} :
∀ (Z : Finset (Set α)), (∀ (z : Set α), z Z) → s ⋃₀ Zz, z Z s z

A set is irreducible if and only if for every cover by a finite collection of closed sets, it is contained in one of the members of the collection.

theorem subset_closure_inter_of_isPreirreducible_of_isOpen {α : Type u} [] {S : Set α} {U : Set α} (hS : ) (hU : ) (h : Set.Nonempty (S U)) :
S closure (S U)

A nonempty open subset of a preirreducible subspace is dense in the subspace.

theorem IsPreirreducible.subset_irreducible {α : Type u} [] {S : Set α} {U : Set α} {Z : Set α} (hZ : ) (hU : ) (hU' : ) (h₁ : U S) (h₂ : S Z) :

If ∅ ≠ U ⊆ S ⊆ Z such that U is open and Z is preirreducible, then S is irreducible.

theorem IsPreirreducible.open_subset {α : Type u} [] {Z : Set α} {U : Set α} (hZ : ) (hU : ) (hU' : U Z) :
theorem IsPreirreducible.interior {α : Type u} [] {Z : Set α} (hZ : ) :
theorem IsPreirreducible.preimage {α : Type u} {β : Type v} [] [] {Z : Set α} (hZ : ) {f : βα} (hf : ) :