@[reducible, inline]

abbrev inducedMetricSubspace {X : Type u_1} (Y : Set X) : Type u_1

Definition 1.15 (Relative topology). Let (X,d) be a metric space and let Y be a subset of X. The induced metric subspace on Y is the metric space (Y, d restricted to Y x Y). A subset E of Y is relatively open in Y if for every y in E there exists r > 0 such that {z in Y | dist y z < r} is contained in E. A subset E of Y is relatively closed in Y if it is closed in the induced metric space, equivalently if Y \ E is relatively open in Y. Used in Proposition 1.18.

Equations

• inducedMetricSubspace Y = { x : X // Y x }

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

A subset E of Y is relatively open in Y if it is open in the metric subspace induced on Y. Used in Proposition 1.18.

Equations

• IsRelOpen Y E = (E.Subset Y ∧ IsOpen (Subtype.val ⁻¹' E))

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

A subset E of Y is relatively closed in Y if it is closed in the metric subspace induced on Y. Used in Proposition 1.18.

Equations

• IsRelClosed Y E = (E.Subset Y ∧ IsClosed (Subtype.val ⁻¹' E))

theorem helperForProposition_1_18_preimage_inter_eq {X : Type u_1} {Y V : Set X} : Subtype.val ⁻¹' V.inter Y = Subtype.val ⁻¹' V

Helper for Proposition 1.18: preimage of an intersection with Y under the subtype inclusion equals the preimage of the first set.

theorem helperForProposition_1_18_eq_inter_of_preimage_eq {X : Type u_1} {Y E V : Set X} (hEY : E ⊆ Y) (hpre : Subtype.val ⁻¹' V = Subtype.val ⁻¹' E) : E = V.inter Y

Helper for Proposition 1.18: recover E = V ∩ Y from equality of preimages.

theorem relOpen_relClosed_iff_eq_inter {X : Type u_1} [MetricSpace X] {Y E : Set X} : (IsRelOpen Y E ↔ ∃ (V : Set X), IsOpen V ∧ E = V.inter Y) ∧ (IsRelClosed Y E ↔ ∃ (K : Set X), IsClosed K ∧ E = K.inter Y)

Proposition 1.18. Let (X,d) be a metric space, let Y be a subset of X, and let E be a subset of Y. (a) E is open in the subspace metric space on Y iff there exists an open set V in X such that E = Set.inter V Y. (b) E is closed in the subspace metric space on Y iff there exists a closed set K in X such that E = Set.inter K Y.

theorem isRelOpen_iff_eq_inter {X : Type u_1} [MetricSpace X] {Y E : Set X} : IsRelOpen Y E ↔ ∃ (V : Set X), IsOpen V ∧ E = V.inter Y

Part (a) for Proposition 1.18: relative openness in Y iff E = Set.inter V Y for some open V in X.

theorem isRelClosed_iff_eq_inter {X : Type u_1} [MetricSpace X] {Y E : Set X} : IsRelClosed Y E ↔ ∃ (K : Set X), IsClosed K ∧ E = K.inter Y

Part (b): relative closedness in Y iff E = Set.inter K Y for some closed K in X. Used in Proposition 1.18.