@[reducible, inline]

abbrev openBall (X : Type u_1) [MetricSpace X] (x0 : X) (r : ℝ) : Set X

Definition 1.10 (Balls): Let (X,d) be a metric space, let x0 ∈ X, and let r > 0. The (open) ball in X centered at x0 with radius r is the set B_{(X,d)}(x0,r) = {x ∈ X : d(x,x0) < r}.

Equations

• openBall X x0 r = Metric.ball x0 r

def IsInteriorPoint {X : Type u_1} [MetricSpace X] (E : Set X) (x : X) : Prop

Definition 1.11 (Interior/exterior/boundary points): Let (X,d) be a metric space and E ⊆ X. (1) x ∈ X is an interior point of E iff there exists r > 0 with B(x,r) ⊆ E. (2) x ∈ X is an exterior point of E iff there exists r > 0 with B(x,r) ⊆ Eᶜ. (3) x ∈ X is a boundary point of E iff for every r > 0, both B(x,r) ∩ E ≠ ∅ and B(x,r) ∩ Eᶜ ≠ ∅.

Equations

• IsInteriorPoint E x = ∃ (r : ℝ), 0 < r ∧ Metric.ball x r ⊆ E

def IsExteriorPoint {X : Type u_1} [MetricSpace X] (E : Set X) (x : X) : Prop

A point is an exterior point of E if some positive ball around it is contained in Eᶜ.

Equations

• IsExteriorPoint E x = ∃ (r : ℝ), 0 < r ∧ Metric.ball x r ⊆ Eᶜ

def IsBoundaryPoint {X : Type u_1} [MetricSpace X] (E : Set X) (x : X) : Prop

A point is a boundary point of E if every positive ball meets both E and Eᶜ.

Equations

• IsBoundaryPoint E x = ∀ (r : ℝ), 0 < r → (Metric.ball x r ∩ E).Nonempty ∧ (Metric.ball x r ∩ Eᶜ).Nonempty

theorem isInteriorPoint_iff_mem_interior {X : Type u_1} [MetricSpace X] (E : Set X) (x : X) : IsInteriorPoint E x ↔ x ∈ interior E

Interior points defined via balls coincide with membership in interior.

theorem isExteriorPoint_iff_mem_interior_compl {X : Type u_1} [MetricSpace X] (E : Set X) (x : X) : IsExteriorPoint E x ↔ x ∈ interior Eᶜ

Exterior points defined via balls coincide with membership in interior of the complement.

theorem mem_closure_iff_forall_ball_inter_nonempty {X : Type u_1} [MetricSpace X] (s : Set X) (x : X) : x ∈ closure s ↔ ∀ (r : ℝ), 0 < r → (Metric.ball x r ∩ s).Nonempty

Characterize closure via nonempty intersections of all positive balls.

theorem isBoundaryPoint_iff_mem_closure_inter_closure_compl {X : Type u_1} [MetricSpace X] (E : Set X) (x : X) : IsBoundaryPoint E x ↔ x ∈ closure E ∩ closure Eᶜ

Boundary points are exactly those in the closures of the set and its complement.

theorem isBoundaryPoint_iff_mem_frontier {X : Type u_1} [MetricSpace X] (E : Set X) (x : X) : IsBoundaryPoint E x ↔ x ∈ frontier E

Boundary points defined via balls coincide with membership in frontier.

def interiorSet {X : Type u_1} [MetricSpace X] (E : Set X) : Set X

Definition 1.12 (Interior, exterior, boundary): Let (X,d) be a metric space and E ⊆ X. (1) x ∈ X is an interior point of E iff there exists r > 0 with B(x,r) ⊆ E. (2) x ∈ X is an exterior point of E iff there exists r > 0 with B(x,r) ∩ E = ∅. (3) x ∈ X is a boundary point of E iff it is neither interior nor exterior. The interior (resp. exterior, boundary) of E is the set of all interior (resp. exterior, boundary) points.

Equations

• interiorSet E = {x : X | IsInteriorPoint E x}

def exteriorSet {X : Type u_1} [MetricSpace X] (E : Set X) : Set X

The exterior set of E as the set of exterior points.

Equations

• exteriorSet E = {x : X | IsExteriorPoint E x}

def boundarySet {X : Type u_1} [MetricSpace X] (E : Set X) : Set X

The boundary set of E as the set of points that are neither interior nor exterior.

Equations

• boundarySet E = {x : X | ¬IsInteriorPoint E x ∧ ¬IsExteriorPoint E x}

theorem interiorSet_eq_interior {X : Type u_1} [MetricSpace X] (E : Set X) : interiorSet E = interior E

The book's interior set agrees with interior.

theorem exteriorSet_eq_interior_compl {X : Type u_1} [MetricSpace X] (E : Set X) : exteriorSet E = interior Eᶜ

The book's exterior set agrees with interior (Eᶜ).

theorem boundarySet_eq_frontier {X : Type u_1} [MetricSpace X] (E : Set X) : boundarySet E = frontier E

The book's boundary set agrees with frontier.

theorem proposition_1_11 {X : Type u_1} [MetricSpace X] (E : Set X) : (∀ x0 ∈ interiorSet E, x0 ∈ E) ∧ (∀ x0 ∈ exteriorSet E, x0 ∉ E) ∧ interiorSet E ∩ exteriorSet E = ∅ ∧ ∀ x0 ∈ boundarySet E, x0 ∈ E ∨ x0 ∉ E

Proposition 1.11: Let (X,d) be a metric space and E ⊆ X. Define int(E) = {x ∈ X : ∃ r > 0, B(x,r) ⊆ E}, ext(E) = int(X \ E), and ∂E = X \ (int(E) ∪ ext(E)), where B(x,r) = {y ∈ X : d(x,y) < r}. Then: (1) If x0 ∈ int(E), then x0 ∈ E. (2) If x0 ∈ ext(E), then x0 ∉ E. (3) int(E) ∩ ext(E) = ∅. (4) If x0 ∈ ∂E, then it is possible that x0 ∈ E and it is possible that x0 ∉ E.

theorem mem_of_mem_interiorSet {X : Type u_1} [MetricSpace X] {E : Set X} {x0 : X} : x0 ∈ interiorSet E → x0 ∈ E

If a point lies in the interior set, then it lies in the set.

theorem mem_compl_of_mem_exteriorSet {X : Type u_1} [MetricSpace X] {E : Set X} {x0 : X} : x0 ∈ exteriorSet E → x0 ∉ E

If a point lies in the exterior set, then it is not in the set.

theorem interiorSet_inter_exteriorSet_eq_empty {X : Type u_1} [MetricSpace X] (E : Set X) : interiorSet E ∩ exteriorSet E = ∅

The interior and exterior sets are disjoint.

theorem mem_or_not_mem_of_mem_boundarySet {X : Type u_1} [MetricSpace X] {E : Set X} {x0 : X} : x0 ∈ boundarySet E → x0 ∈ E ∨ x0 ∉ E

A boundary point may or may not lie in the set.

theorem helperForProposition_1_12_one_lt_two : 1 < 2

Helper for Proposition 1.12: 1 < 2 in ℝ.

theorem helperForProposition_1_12_interior_Ico : interior (Set.Ico 1 2) = Set.Ioo 1 2

Helper for Proposition 1.12: interior of Ico is Ioo.

theorem helperForProposition_1_12_interior_compl_Ico : interior (Set.Ico 1 2)ᶜ = Set.Iio 1 ∪ Set.Ioi 2

Helper for Proposition 1.12: interior of the complement of Ico.

theorem helperForProposition_1_12_frontier_Ico : frontier (Set.Ico 1 2) = {1, 2}

Helper for Proposition 1.12: frontier of Ico is {1,2}.

theorem real_Ico_interior_exterior_boundary : have E := Set.Ico 1 2; interior E = Set.Ioo 1 2 ∧ interior Eᶜ = Set.Iio 1 ∪ Set.Ioi 2 ∧ frontier E = {1, 2} ∧ 1 ∈ E ∩ frontier E ∧ 2 ∈ frontier E \ E

Proposition 1.12: Let E = [1,2) ⊆ ℝ with the standard metric. Then interior E = (1,2), interior (Eᶜ) = (-∞,1) ∪ (2,∞), and frontier E = {1,2}. In particular, 1 ∈ E ∩ frontier E and 2 ∈ frontier E \ E.

theorem helperForProposition_1_13_exists_ball_subset_singleton {X : Type u_1} [MetricSpace X] [DiscreteTopology X] (x : X) : ∃ (r : ℝ), 0 < r ∧ Metric.ball x r ⊆ {x}

Helper for Proposition 1.13: a singleton contains a positive-radius ball.

theorem helperForProposition_1_13_mem_interiorSet_of_mem {X : Type u_1} [MetricSpace X] [DiscreteTopology X] {E : Set X} {x : X} : x ∈ E → x ∈ interiorSet E

Helper for Proposition 1.13: points of E are interior points in the discrete topology.

theorem helperForProposition_1_13_mem_exteriorSet_of_mem_compl {X : Type u_1} [MetricSpace X] [DiscreteTopology X] {E : Set X} {x : X} : x ∈ Eᶜ → x ∈ exteriorSet E

Helper for Proposition 1.13: points of Eᶜ are exterior points in the discrete topology.

theorem helperForProposition_1_13_boundarySet_eq_empty {X : Type u_1} [MetricSpace X] [DiscreteTopology X] (E : Set X) : boundarySet E = ∅

Helper for Proposition 1.13: the boundary set is empty in the discrete topology.

theorem proposition_1_13 {X : Type u_1} [MetricSpace X] [DiscreteTopology X] (E : Set X) : interiorSet E = E ∧ exteriorSet E = Eᶜ ∧ boundarySet E = ∅

Proposition 1.13: Let X be a set equipped with the discrete metric d_disc with d_disc(x,y)=0 if x=y and d_disc(x,y)=1 if x≠y. For every E ⊆ X, int(E)=E, ext(E)=X \ E, and ∂E=∅.

def closureSet {X : Type u_1} [MetricSpace X] (E : Set X) : Set X

Definition 1.13 (Closure): Let (X,d) be a metric space and E ⊆ X. A point x ∈ X is an adherent point of E iff for every r > 0, B(x,r) ∩ E ≠ ∅, where B(x,r) = {y ∈ X : d(x,y) < r}. The closure \overline{E} is the set of all adherent points: \overline{E} = {x ∈ X : ∀ r > 0, B(x,r) ∩ E ≠ ∅}.

Equations

• closureSet E = {x : X | ∀ (r : ℝ), 0 < r → (Metric.ball x r ∩ E).Nonempty}

def IsAdherentPoint {X : Type u_1} [MetricSpace X] (E : Set X) (x : X) : Prop

A point is adherent to E if every positive ball around it meets E.

Equations

• IsAdherentPoint E x = ∀ (r : ℝ), 0 < r → (Metric.ball x r ∩ E).Nonempty

theorem isAdherentPoint_iff_mem_closure {X : Type u_1} [MetricSpace X] (E : Set X) (x : X) : IsAdherentPoint E x ↔ x ∈ closure E

Adherent points coincide with membership in closure.

theorem closureSet_eq_setOf_isAdherentPoint {X : Type u_1} [MetricSpace X] (E : Set X) : closureSet E = {x : X | IsAdherentPoint E x}

The closure of E as the set of adherent points.

theorem closureSet_eq_closure {X : Type u_1} [MetricSpace X] (E : Set X) : closureSet E = closure E

The book's closure set agrees with closure.

theorem helperForProposition_1_14_isAdherentPoint_iff_mem_closure {X : Type u_1} [MetricSpace X] (E : Set X) (x0 : X) : IsAdherentPoint E x0 ↔ x0 ∈ closure E

Helper for Proposition 1.14: adherent points coincide with closure membership.

theorem helperForProposition_1_14_adherent_iff_interior_or_boundary {X : Type u_1} [MetricSpace X] (E : Set X) (x0 : X) : IsAdherentPoint E x0 ↔ IsInteriorPoint E x0 ∨ IsBoundaryPoint E x0

Helper for Proposition 1.14: adherent points are interior or boundary points.

theorem helperForProposition_1_14_adherent_iff_exists_seq_tendsto {X : Type u_1} [MetricSpace X] (E : Set X) (x0 : X) : IsAdherentPoint E x0 ↔ ∃ (u : ℕ → X), (∀ (n : ℕ), u n ∈ E) ∧ Filter.Tendsto u Filter.atTop (nhds x0)

Helper for Proposition 1.14: adherent points admit convergent sequences from the set.

theorem proposition_1_14 {X : Type u_1} [MetricSpace X] (E : Set X) (x0 : X) : (IsAdherentPoint E x0 ↔ IsInteriorPoint E x0 ∨ IsBoundaryPoint E x0) ∧ (IsAdherentPoint E x0 ↔ ∃ (u : ℕ → X), (∀ (n : ℕ), u n ∈ E) ∧ Filter.Tendsto u Filter.atTop (nhds x0))

Proposition 1.14: Let (X,d) be a metric space, E ⊆ X, and x0 ∈ X. The following are equivalent: (a) x0 is adherent to E, i.e., every r > 0 has B(x0,r) ∩ E ≠ ∅; (b) x0 is either an interior point of E or a boundary point of E; (c) there exists a sequence (x_n) in E with x_n → x0.

theorem helperForTheorem_1_3_closureSet_eq_compl_exteriorSet {X : Type u_1} [MetricSpace X] (E : Set X) : closureSet E = (exteriorSet E)ᶜ

Helper for Theorem 1.3: the closure set is the complement of the exterior set.

theorem helperForTheorem_1_3_interiorSet_union_boundarySet_eq_compl_exteriorSet {X : Type u_1} [MetricSpace X] (E : Set X) : interiorSet E ∪ boundarySet E = (exteriorSet E)ᶜ

Helper for Theorem 1.3: interior union boundary equals the complement of the exterior set.

theorem closureSet_eq_interiorSet_union_boundarySet_and_compl_exteriorSet {X : Type u_1} [MetricSpace X] (E : Set X) : closureSet E = interiorSet E ∪ boundarySet E ∧ closureSet E = (exteriorSet E)ᶜ

Theorem 1.3: Let (X,d) be a metric space and E ⊆ X. Define int(E) = {x ∈ X : ∃ r > 0, B(x,r) ⊆ E}, ext(E) = int(X \ E), ∂E = X \ (int(E) ∪ ext(E)), and \overline{E} = {x ∈ X : ∀ r > 0, B(x,r) ∩ E ≠ ∅}. Then \overline{E} = int(E) ∪ ∂E = X \ ext(E).

theorem closureSet_eq_interiorSet_union_boundarySet_and_compl_exteriorSet' {X : Type u_1} [MetricSpace X] (E : Set X) : closureSet E = interiorSet E ∪ boundarySet E ∧ closureSet E = (exteriorSet E)ᶜ

The closure equals the union of the interior and boundary, and equals the complement of the exterior.

def IsClosedSet {X : Type u_1} [MetricSpace X] (E : Set X) : Prop

Definition 1.14 (Open and closed sets): Let (X,d) be a metric space and E ⊆ X. The set E is called closed if ∂E ⊆ E. The set E is called open if ∂E ∩ E = ∅.

Equations

• IsClosedSet E = (frontier E ⊆ E)

def IsOpenSet {X : Type u_1} [MetricSpace X] (E : Set X) : Prop

A set is open in the book's sense if its frontier is disjoint from it.

Equations

• IsOpenSet E = (frontier E ∩ E = ∅)

theorem isClosedSet_iff_isClosed {X : Type u_1} [MetricSpace X] (E : Set X) : IsClosedSet E ↔ IsClosed E

The book's closed-set predicate is equivalent to IsClosed.

theorem isOpenSet_iff_isOpen {X : Type u_1} [MetricSpace X] (E : Set X) : IsOpenSet E ↔ IsOpen E

The book's open-set predicate is equivalent to IsOpen.

theorem proposition_1_15 {X : Type u_1} [MetricSpace X] : IsOpen Set.univ ∧ IsClosed Set.univ ∧ IsOpen ∅ ∧ IsClosed ∅

Proposition 1.15: Let (X,d) be a metric space. Then X and ∅ are both open and closed subsets of X.

theorem open_closed_univ_empty {X : Type u_1} [MetricSpace X] : IsOpen Set.univ ∧ IsClosed Set.univ ∧ IsOpen ∅ ∧ IsClosed ∅

In a metric space, Set.univ and ∅ are both open and closed.

theorem proposition_1_16 {X : Type u_1} [MetricSpace X] [DiscreteTopology X] (E : Set X) : IsOpen E ∧ IsClosed E

Proposition 1.16: Let (X, d_disc) be a set equipped with the discrete metric d_disc(x,y)=0 if x=y and d_disc(x,y)=1 if x≠y. Then every subset E ⊆ X is open and closed in the metric topology induced by d_disc.

theorem helperForProposition_1_17_part_a {X : Type u_1} [MetricSpace X] (E : Set X) : (IsOpen E ↔ E = interior E) ∧ (IsOpen E ↔ ∀ x ∈ E, ∃ (r : ℝ), 0 < r ∧ Metric.ball x r ⊆ E)

Helper for Proposition 1.17: the two characterizations of open sets in part (a).

theorem helperForProposition_1_17_part_b {X : Type u_1} [MetricSpace X] (E : Set X) : (IsClosed E ↔ ∀ (x : X), IsAdherentPoint E x → x ∈ E) ∧ (IsClosed E ↔ ∀ (u : ℕ → X), (∀ (n : ℕ), u n ∈ E) → ∀ (x : X), Filter.Tendsto u Filter.atTop (nhds x) → x ∈ E)

Helper for Proposition 1.17: closed sets via adherent points and sequential limits.

theorem helperForProposition_1_17_parts_c_to_g {X : Type u_1} [MetricSpace X] : (∀ (x0 : X) (r : ℝ), 0 < r → IsOpen (Metric.ball x0 r) ∧ IsClosed (Metric.closedBall x0 r)) ∧ (∀ (x0 : X), IsClosed {x0}) ∧ (∀ (E : Set X), IsOpen E ↔ IsClosed Eᶜ) ∧ (∀ (n : ℕ) (E : Fin n → Set X), (∀ (i : Fin n), IsOpen (E i)) → IsOpen (⋂ (i : Fin n), E i)) ∧ (∀ (n : ℕ) (F : Fin n → Set X), (∀ (i : Fin n), IsClosed (F i)) → IsClosed (⋃ (i : Fin n), F i)) ∧ (∀ {I : Type u_2} (E : I → Set X), (∀ (i : I), IsOpen (E i)) → IsOpen (⋃ (i : I), E i)) ∧ ∀ {I : Type u_3} (F : I → Set X), (∀ (i : I), IsClosed (F i)) → IsClosed (⋂ (i : I), F i)

Helper for Proposition 1.17: parts (c)-(g) on balls, complements, and unions/intersections.

theorem helperForProposition_1_17_part_h {X : Type u_1} [MetricSpace X] (E : Set X) : IsOpen (interior E) ∧ interior E ⊆ E ∧ (∀ (V : Set X), IsOpen V → V ⊆ E → V ⊆ interior E) ∧ IsClosed (closure E) ∧ E ⊆ closure E ∧ ∀ (K : Set X), IsClosed K → E ⊆ K → closure E ⊆ K

Helper for Proposition 1.17: interior is maximal open, closure is minimal closed.

theorem proposition_1_17 {X : Type u_1} [MetricSpace X] : (∀ (E : Set X), (IsOpen E ↔ E = interior E) ∧ (IsOpen E ↔ ∀ x ∈ E, ∃ (r : ℝ), 0 < r ∧ Metric.ball x r ⊆ E)) ∧ (∀ (E : Set X), (IsClosed E ↔ ∀ (x : X), IsAdherentPoint E x → x ∈ E) ∧ (IsClosed E ↔ ∀ (u : ℕ → X), (∀ (n : ℕ), u n ∈ E) → ∀ (x : X), Filter.Tendsto u Filter.atTop (nhds x) → x ∈ E)) ∧ (∀ (x0 : X) (r : ℝ), 0 < r → IsOpen (Metric.ball x0 r) ∧ IsClosed (Metric.closedBall x0 r)) ∧ (∀ (x0 : X), IsClosed {x0}) ∧ (∀ (E : Set X), IsOpen E ↔ IsClosed Eᶜ) ∧ (∀ (n : ℕ) (E : Fin n → Set X), (∀ (i : Fin n), IsOpen (E i)) → IsOpen (⋂ (i : Fin n), E i)) ∧ (∀ (n : ℕ) (F : Fin n → Set X), (∀ (i : Fin n), IsClosed (F i)) → IsClosed (⋃ (i : Fin n), F i)) ∧ (∀ {I : Type u_2} (E : I → Set X), (∀ (i : I), IsOpen (E i)) → IsOpen (⋃ (i : I), E i)) ∧ (∀ {I : Type u_3} (F : I → Set X), (∀ (i : I), IsClosed (F i)) → IsClosed (⋂ (i : I), F i)) ∧ ∀ (E : Set X), IsOpen (interior E) ∧ interior E ⊆ E ∧ (∀ (V : Set X), IsOpen V → V ⊆ E → V ⊆ interior E) ∧ IsClosed (closure E) ∧ E ⊆ closure E ∧ ∀ (K : Set X), IsClosed K → E ⊆ K → closure E ⊆ K

Proposition 1.17 (Basic properties of open and closed sets): Let (X,d) be a metric space. (a) For E ⊆ X, E is open iff E = int(E); equivalently, E is open iff for every x ∈ E there exists r > 0 such that B(x,r) ⊆ E. (b) For E ⊆ X, E is closed iff it contains all its adherent points; equivalently, E is closed iff every convergent sequence in E has its limit in E. (c) For x0 ∈ X and r > 0, B(x0,r) is open and {x ∈ X : d(x,x0) ≤ r} is closed. (d) For x0 ∈ X, the singleton {x0} is closed. (e) For E ⊆ X, E is open iff X \ E is closed. (f) Finite intersections of open sets are open; finite unions of closed sets are closed. (g) Arbitrary unions of open sets are open; arbitrary intersections of closed sets are closed. (h) For E ⊆ X, int(E) is the largest open set contained in E, and \overline{E} is the smallest closed set containing E.

theorem proposition_1_17' {X : Type u_1} [MetricSpace X] : (∀ (E : Set X), (IsOpen E ↔ E = interior E) ∧ (IsOpen E ↔ ∀ x ∈ E, ∃ (r : ℝ), 0 < r ∧ Metric.ball x r ⊆ E)) ∧ (∀ (E : Set X), (IsClosed E ↔ ∀ (x : X), IsAdherentPoint E x → x ∈ E) ∧ (IsClosed E ↔ ∀ (u : ℕ → X), (∀ (n : ℕ), u n ∈ E) → ∀ (x : X), Filter.Tendsto u Filter.atTop (nhds x) → x ∈ E)) ∧ (∀ (x0 : X) (r : ℝ), 0 < r → IsOpen (Metric.ball x0 r) ∧ IsClosed (Metric.closedBall x0 r)) ∧ (∀ (x0 : X), IsClosed {x0}) ∧ (∀ (E : Set X), IsOpen E ↔ IsClosed Eᶜ) ∧ (∀ (n : ℕ) (E : Fin n → Set X), (∀ (i : Fin n), IsOpen (E i)) → IsOpen (⋂ (i : Fin n), E i)) ∧ (∀ (n : ℕ) (F : Fin n → Set X), (∀ (i : Fin n), IsClosed (F i)) → IsClosed (⋃ (i : Fin n), F i)) ∧ (∀ {I : Type u_2} (E : I → Set X), (∀ (i : I), IsOpen (E i)) → IsOpen (⋃ (i : I), E i)) ∧ (∀ {I : Type u_3} (F : I → Set X), (∀ (i : I), IsClosed (F i)) → IsClosed (⋂ (i : I), F i)) ∧ ∀ (E : Set X), IsOpen (interior E) ∧ interior E ⊆ E ∧ (∀ (V : Set X), IsOpen V → V ⊆ E → V ⊆ interior E) ∧ IsClosed (closure E) ∧ E ⊆ closure E ∧ ∀ (K : Set X), IsClosed K → E ⊆ K → closure E ⊆ K

Basic properties of open and closed sets in a metric space (Proposition 1.17).

theorem real_Ico_one_two_not_isOpen : ¬IsOpen (Set.Ico 1 2)

Helper for Proposition 1.35: Ico (1,2) is not open in ℝ.

theorem real_Ico_one_two_not_isClosed : ¬IsClosed (Set.Ico 1 2)

Helper for Proposition 1.35: Ico (1,2) is not closed in ℝ.

theorem ulift_Ico_one_two_not_isOpen : ¬IsOpen (ULift.down ⁻¹' Set.Ico 1 2)

Helper for Proposition 1.35: the lifted Ico (1,2) is not open.

theorem ulift_Ico_one_two_not_isClosed : ¬IsClosed (ULift.down ⁻¹' Set.Ico 1 2)

Helper for Proposition 1.35: the lifted Ico (1,2) is not closed.

theorem proposition_1_35 : (∀ {X : Type u_1} [inst : MetricSpace X], IsOpen Set.univ ∧ IsClosed Set.univ ∧ IsOpen ∅ ∧ IsClosed ∅) ∧ (∃ (X : Type u_2) (h : MetricSpace X) (E : Set X), ¬IsOpen E ∧ ¬IsClosed E) ∧ ∀ {X : Type u_3} [inst : MetricSpace X] (E : Set X), IsOpen E ↔ IsClosed Eᶜ

Proposition 1.35 (Open and closed are not complementary notions): Let (X,d) be a metric space. (1) There exist subsets of X that are both open and closed (e.g., X itself and ∅). (2) There may exist subsets of X that are neither open nor closed. (3) A subset E ⊆ X is open iff its complement X \ E is closed. In particular, knowing that a set is not open does not imply that it is closed, and vice versa.