mathlib3 documentation

topology.inseparable

Inseparable points in a topological space #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we define

We also prove various basic properties of the relation inseparable.

Notations #

Tags #

topological space, separation setoid

specializes relation #

source
def specializes {X : Type u_1} [topological_space X] (x y : X) :
Prop

x specializes to y (notation: x ⤳ y) if either of the following equivalent properties hold:

  • 𝓝 x ≤ 𝓝 y; this property is used as the definition;
  • pure x ≤ 𝓝 y; in other words, any neighbourhood of y contains x;
  • y ∈ closure {x};
  • closure {y} ⊆ closure {x};
  • for any closed set s we have x ∈ s → y ∈ s;
  • for any open set s we have y ∈ s → x ∈ s;
  • y is a cluster point of the filter pure x = 𝓟 {x}.

This relation defines a preorder on X. If X is a T₀ space, then this preorder is a partial order. If X is a T₁ space, then this partial order is trivial : x ⤳ y ↔ x = y.

Equations
source
theorem specializes_tfae {X : Type u_1} [topological_space X] (x y : X) :
[x ⤳ y, has_pure.pure x ≤ nhds y, ∀ (s : set X), is_open s → y ∈ s → x ∈ s, ∀ (s : set X), is_closed s → x ∈ s → y ∈ s, y ∈ closure {x}, closure {y} ⊆ closure {x}, cluster_pt y (has_pure.pure x)].tfae

A collection of equivalent definitions of x ⤳ y. The public API is given by iff lemmas below.

source
theorem specializes_iff_nhds {X : Type u_1} [topological_space X] {x y : X} :
x ⤳ y ↔ nhds x ≤ nhds y
source
theorem specializes_iff_pure {X : Type u_1} [topological_space X] {x y : X} :
x ⤳ y ↔ has_pure.pure x ≤ nhds y
source
theorem specializes.nhds_le_nhds {X : Type u_1} [topological_space X] {x y : X} :
x ⤳ y → nhds x ≤ nhds y

Alias of the forward direction of specializes_iff_nhds.

source
theorem specializes.pure_le_nhds {X : Type u_1} [topological_space X] {x y : X} :
x ⤳ y → has_pure.pure x ≤ nhds y

Alias of the forward direction of specializes_iff_pure.

source
theorem specializes_iff_forall_open {X : Type u_1} [topological_space X] {x y : X} :
x ⤳ y ↔ ∀ (s : set X), is_open s → y ∈ s → x ∈ s
source
theorem specializes.mem_open {X : Type u_1} [topological_space X] {x y : X} {s : set X} (h : x ⤳ y) (hs : is_open s) (hy : y ∈ s) :
x ∈ s
source
theorem is_open.not_specializes {X : Type u_1} [topological_space X] {x y : X} {s : set X} (hs : is_open s) (hx : x ∉ s) (hy : y ∈ s) :
¬x ⤳ y
source
theorem specializes_iff_forall_closed {X : Type u_1} [topological_space X] {x y : X} :
x ⤳ y ↔ ∀ (s : set X), is_closed s → x ∈ s → y ∈ s
source
theorem specializes.mem_closed {X : Type u_1} [topological_space X] {x y : X} {s : set X} (h : x ⤳ y) (hs : is_closed s) (hx : x ∈ s) :
y ∈ s
source
theorem is_closed.not_specializes {X : Type u_1} [topological_space X] {x y : X} {s : set X} (hs : is_closed s) (hx : x ∈ s) (hy : y ∉ s) :
¬x ⤳ y
source
theorem specializes_iff_mem_closure {X : Type u_1} [topological_space X] {x y : X} :
x ⤳ y ↔ y ∈ closure {x}
source
theorem specializes.mem_closure {X : Type u_1} [topological_space X] {x y : X} :
x ⤳ y → y ∈ closure {x}

Alias of the forward direction of specializes_iff_mem_closure.

source
theorem specializes_iff_closure_subset {X : Type u_1} [topological_space X] {x y : X} :
x ⤳ y ↔ closure {y} ⊆ closure {x}
source
theorem specializes.closure_subset {X : Type u_1} [topological_space X] {x y : X} :
x ⤳ y → closure {y} ⊆ closure {x}

Alias of the forward direction of specializes_iff_closure_subset.

source
theorem filter.has_basis.specializes_iff {X : Type u_1} [topological_space X] {x y : X} {ι : Sort u_2} {p : ι → Prop} {s : ι → set X} (h : (nhds y).has_basis p s) :
x ⤳ y ↔ ∀ (i : ι), p i → x ∈ s i
source
theorem specializes_rfl {X : Type u_1} [topological_space X] {x : X} :
x ⤳ x
source
@[refl]
theorem specializes_refl {X : Type u_1} [topological_space X] (x : X) :
x ⤳ x
source
@[trans]
theorem specializes.trans {X : Type u_1} [topological_space X] {x y z : X} :
x ⤳ y → y ⤳ z → x ⤳ z
source
theorem specializes_of_eq {X : Type u_1} [topological_space X] {x y : X} (e : x = y) :
x ⤳ y
source
theorem specializes_of_nhds_within {X : Type u_1} [topological_space X] {x y : X} {s : set X} (h₁ : nhds_within x s ≤ nhds_within y s) (h₂ : x ∈ s) :
x ⤳ y
source
theorem specializes.map_of_continuous_at {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] {x y : X} {f : X → Y} (h : x ⤳ y) (hy : continuous_at f y) :
f x ⤳ f y
source
theorem specializes.map {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] {x y : X} {f : X → Y} (h : x ⤳ y) (hf : continuous f) :
f x ⤳ f y
source
theorem inducing.specializes_iff {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] {x y : X} {f : X → Y} (hf : inducing f) :
f x ⤳ f y ↔ x ⤳ y
source
theorem subtype_specializes_iff {X : Type u_1} [topological_space X] {p : X → Prop} (x y : subtype p) :
x ⤳ y ↔ ↑x ⤳ ↑y
source
@[simp]
theorem specializes_prod {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] {x₁ x₂ : X} {y₁ y₂ : Y} :
(x₁, y₁) ⤳ (x₂, y₂) ↔ x₁ ⤳ x₂ ∧ y₁ ⤳ y₂
source
theorem specializes.prod {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] {x₁ x₂ : X} {y₁ y₂ : Y} (hx : x₁ ⤳ x₂) (hy : y₁ ⤳ y₂) :
(x₁, y₁) ⤳ (x₂, y₂)
source
@[simp]
theorem specializes_pi {ι : Type u_5} {π : ι → Type u_6} [Π (i : ι), topological_space (π i)] {f g : Π (i : ι), π i} :
f ⤳ g ↔ ∀ (i : ι), f i ⤳ g i
source
theorem not_specializes_iff_exists_open {X : Type u_1} [topological_space X] {x y : X} :
¬x ⤳ y ↔ ∃ (S : set X), is_open S ∧ y ∈ S ∧ x ∉ S
source
theorem not_specializes_iff_exists_closed {X : Type u_1} [topological_space X] {x y : X} :
¬x ⤳ y ↔ ∃ (S : set X), is_closed S ∧ x ∈ S ∧ y ∉ S
source
def specialization_preorder (X : Type u_1) [topological_space X] :
preorder X

Specialization forms a preorder on the topological space.

Equations
source
theorem continuous.specialization_monotone {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] {f : X → Y} (hf : continuous f) :
monotone f

A continuous function is monotone with respect to the specialization preorders on the domain and the codomain.

inseparable relation #

source
def inseparable {X : Type u_1} [topological_space X] (x y : X) :
Prop

Two points x and y in a topological space are inseparable if any of the following equivalent properties hold:

Equations
source
theorem inseparable_def {X : Type u_1} [topological_space X] {x y : X} :
inseparable x y ↔ nhds x = nhds y
source
theorem inseparable_iff_specializes_and {X : Type u_1} [topological_space X] {x y : X} :
inseparable x y ↔ x ⤳ y ∧ y ⤳ x
source
theorem inseparable.specializes {X : Type u_1} [topological_space X] {x y : X} (h : inseparable x y) :
x ⤳ y
source
theorem inseparable.specializes' {X : Type u_1} [topological_space X] {x y : X} (h : inseparable x y) :
y ⤳ x
source
theorem specializes.antisymm {X : Type u_1} [topological_space X] {x y : X} (h₁ : x ⤳ y) (h₂ : y ⤳ x) :
inseparable x y
source
theorem inseparable_iff_forall_open {X : Type u_1} [topological_space X] {x y : X} :
inseparable x y ↔ ∀ (s : set X), is_open s → (x ∈ s ↔ y ∈ s)
source
theorem not_inseparable_iff_exists_open {X : Type u_1} [topological_space X] {x y : X} :
¬inseparable x y ↔ ∃ (s : set X), is_open s ∧ xor (x ∈ s) (y ∈ s)
source
theorem inseparable_iff_forall_closed {X : Type u_1} [topological_space X] {x y : X} :
inseparable x y ↔ ∀ (s : set X), is_closed s → (x ∈ s ↔ y ∈ s)
source
theorem inseparable_iff_mem_closure {X : Type u_1} [topological_space X] {x y : X} :
inseparable x y ↔ x ∈ closure {y} ∧ y ∈ closure {x}
source
theorem inseparable_iff_closure_eq {X : Type u_1} [topological_space X] {x y : X} :
inseparable x y ↔ closure {x} = closure {y}
source
theorem inseparable_of_nhds_within_eq {X : Type u_1} [topological_space X] {x y : X} {s : set X} (hx : x ∈ s) (hy : y ∈ s) (h : nhds_within x s = nhds_within y s) :
inseparable x y
source
theorem inducing.inseparable_iff {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] {x y : X} {f : X → Y} (hf : inducing f) :
inseparable (f x) (f y) ↔ inseparable x y
source
theorem subtype_inseparable_iff {X : Type u_1} [topological_space X] {p : X → Prop} (x y : subtype p) :
inseparable x y ↔ inseparable ↑x ↑y
source
@[simp]
theorem inseparable_prod {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] {x₁ x₂ : X} {y₁ y₂ : Y} :
inseparable (x₁, y₁) (x₂, y₂) ↔ inseparable x₁ x₂ ∧ inseparable y₁ y₂
source
theorem inseparable.prod {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] {x₁ x₂ : X} {y₁ y₂ : Y} (hx : inseparable x₁ x₂) (hy : inseparable y₁ y₂) :
inseparable (x₁, y₁) (x₂, y₂)
source
@[simp]
theorem inseparable_pi {ι : Type u_5} {π : ι → Type u_6} [Π (i : ι), topological_space (π i)] {f g : Π (i : ι), π i} :
inseparable f g ↔ ∀ (i : ι), inseparable (f i) (g i)
source
@[refl]
theorem inseparable.refl {X : Type u_1} [topological_space X] (x : X) :
inseparable x x
source
theorem inseparable.rfl {X : Type u_1} [topological_space X] {x : X} :
inseparable x x
source
theorem inseparable.of_eq {X : Type u_1} [topological_space X] {x y : X} (e : x = y) :
inseparable x y
source
@[symm]
theorem inseparable.symm {X : Type u_1} [topological_space X] {x y : X} (h : inseparable x y) :
inseparable y x
source
@[trans]
theorem inseparable.trans {X : Type u_1} [topological_space X] {x y z : X} (h₁ : inseparable x y) (h₂ : inseparable y z) :
inseparable x z
source
theorem inseparable.nhds_eq {X : Type u_1} [topological_space X] {x y : X} (h : inseparable x y) :
nhds x = nhds y
source
theorem inseparable.mem_open_iff {X : Type u_1} [topological_space X] {x y : X} {s : set X} (h : inseparable x y) (hs : is_open s) :
x ∈ s ↔ y ∈ s
source
theorem inseparable.mem_closed_iff {X : Type u_1} [topological_space X] {x y : X} {s : set X} (h : inseparable x y) (hs : is_closed s) :
x ∈ s ↔ y ∈ s
source
theorem inseparable.map_of_continuous_at {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] {x y : X} {f : X → Y} (h : inseparable x y) (hx : continuous_at f x) (hy : continuous_at f y) :
inseparable (f x) (f y)
source
theorem inseparable.map {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] {x y : X} {f : X → Y} (h : inseparable x y) (hf : continuous f) :
inseparable (f x) (f y)
source
theorem is_closed.not_inseparable {X : Type u_1} [topological_space X] {x y : X} {s : set X} (hs : is_closed s) (hx : x ∈ s) (hy : y ∉ s) :
¬inseparable x y
source
theorem is_open.not_inseparable {X : Type u_1} [topological_space X] {x y : X} {s : set X} (hs : is_open s) (hx : x ∈ s) (hy : y ∉ s) :
¬inseparable x y

Separation quotient #

In this section we define the quotient of a topological space by the inseparable relation.

source
def inseparable_setoid (X : Type u_1) [topological_space X] :
setoid X

A setoid version of inseparable, used to define the separation_quotient.

Equations
source
@[protected, instance]
def separation_quotient.topological_space (X : Type u_1) [topological_space X] :
topological_space (separation_quotient X)
source
def separation_quotient (X : Type u_1) [topological_space X] :
Type u_1

The quotient of a topological space by its inseparable_setoid. This quotient is guaranteed to be a T₀ space.

Equations
Instances for separation_quotient
source
def separation_quotient.mk {X : Type u_1} [topological_space X] :
X → separation_quotient X

The natural map from a topological space to its separation quotient.

Equations
source
theorem separation_quotient.quotient_map_mk {X : Type u_1} [topological_space X] :
quotient_map separation_quotient.mk
source
theorem separation_quotient.continuous_mk {X : Type u_1} [topological_space X] :
continuous separation_quotient.mk
source
@[simp]
theorem separation_quotient.mk_eq_mk {X : Type u_1} [topological_space X] {x y : X} :
separation_quotient.mk x = separation_quotient.mk y ↔ inseparable x y
source
theorem separation_quotient.surjective_mk {X : Type u_1} [topological_space X] :
function.surjective separation_quotient.mk
source
@[simp]
theorem separation_quotient.range_mk {X : Type u_1} [topological_space X] :
set.range separation_quotient.mk = set.univ
source
@[protected, instance]
def separation_quotient.nonempty {X : Type u_1} [topological_space X] [nonempty X] :
nonempty (separation_quotient X)
source
@[protected, instance]
def separation_quotient.inhabited {X : Type u_1} [topological_space X] [inhabited X] :
inhabited (separation_quotient X)
Equations
source
@[protected, instance]
def separation_quotient.subsingleton {X : Type u_1} [topological_space X] [subsingleton X] :
subsingleton (separation_quotient X)
source
theorem separation_quotient.preimage_image_mk_open {X : Type u_1} [topological_space X] {s : set X} (hs : is_open s) :
separation_quotient.mk ⁻¹' (separation_quotient.mk '' s) = s
source
theorem separation_quotient.is_open_map_mk {X : Type u_1} [topological_space X] :
is_open_map separation_quotient.mk
source
theorem separation_quotient.preimage_image_mk_closed {X : Type u_1} [topological_space X] {s : set X} (hs : is_closed s) :
separation_quotient.mk ⁻¹' (separation_quotient.mk '' s) = s
source
theorem separation_quotient.inducing_mk {X : Type u_1} [topological_space X] :
inducing separation_quotient.mk
source
theorem separation_quotient.is_closed_map_mk {X : Type u_1} [topological_space X] :
is_closed_map separation_quotient.mk
source
@[simp]
theorem separation_quotient.comap_mk_nhds_mk {X : Type u_1} [topological_space X] {x : X} :
filter.comap separation_quotient.mk (nhds (separation_quotient.mk x)) = nhds x
source
@[simp]
theorem separation_quotient.comap_mk_nhds_set_image {X : Type u_1} [topological_space X] {s : set X} :
filter.comap separation_quotient.mk (nhds_set (separation_quotient.mk '' s)) = nhds_set s
source
theorem separation_quotient.map_mk_nhds {X : Type u_1} [topological_space X] {x : X} :
filter.map separation_quotient.mk (nhds x) = nhds (separation_quotient.mk x)
source
theorem separation_quotient.map_mk_nhds_set {X : Type u_1} [topological_space X] {s : set X} :
filter.map separation_quotient.mk (nhds_set s) = nhds_set (separation_quotient.mk '' s)
source
theorem separation_quotient.comap_mk_nhds_set {X : Type u_1} [topological_space X] {t : set (separation_quotient X)} :
filter.comap separation_quotient.mk (nhds_set t) = nhds_set (separation_quotient.mk ⁻¹' t)
source
theorem separation_quotient.preimage_mk_closure {X : Type u_1} [topological_space X] {t : set (separation_quotient X)} :
separation_quotient.mk ⁻¹' closure t = closure (separation_quotient.mk ⁻¹' t)
source
theorem separation_quotient.preimage_mk_interior {X : Type u_1} [topological_space X] {t : set (separation_quotient X)} :
separation_quotient.mk ⁻¹' interior t = interior (separation_quotient.mk ⁻¹' t)
source
theorem separation_quotient.preimage_mk_frontier {X : Type u_1} [topological_space X] {t : set (separation_quotient X)} :
separation_quotient.mk ⁻¹' frontier t = frontier (separation_quotient.mk ⁻¹' t)
source
theorem separation_quotient.image_mk_closure {X : Type u_1} [topological_space X] {s : set X} :
separation_quotient.mk '' closure s = closure (separation_quotient.mk '' s)
source
theorem separation_quotient.map_prod_map_mk_nhds {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] (x : X) (y : Y) :
filter.map (prod.map separation_quotient.mk separation_quotient.mk) (nhds (x, y)) = nhds (separation_quotient.mk x, separation_quotient.mk y)
source
theorem separation_quotient.map_mk_nhds_within_preimage {X : Type u_1} [topological_space X] (s : set (separation_quotient X)) (x : X) :
filter.map separation_quotient.mk (nhds_within x (separation_quotient.mk ⁻¹' s)) = nhds_within (separation_quotient.mk x) s
source
def separation_quotient.lift {X : Type u_1} {α : Type u_4} [topological_space X] (f : X → α) (hf : ∀ (x y : X), inseparable x y → f x = f y) :
separation_quotient X → α

Lift a map f : X → α such that inseparable x y → f x = f y to a map separation_quotient X → α.

Equations
source
@[simp]
theorem separation_quotient.lift_mk {X : Type u_1} {α : Type u_4} [topological_space X] {f : X → α} (hf : ∀ (x y : X), inseparable x y → f x = f y) (x : X) :
separation_quotient.lift f hf (separation_quotient.mk x) = f x
source
@[simp]
theorem separation_quotient.lift_comp_mk {X : Type u_1} {α : Type u_4} [topological_space X] {f : X → α} (hf : ∀ (x y : X), inseparable x y → f x = f y) :
separation_quotient.lift f hf ∘ separation_quotient.mk = f
source
@[simp]
theorem separation_quotient.tendsto_lift_nhds_mk {X : Type u_1} {α : Type u_4} [topological_space X] {f : X → α} {hf : ∀ (x y : X), inseparable x y → f x = f y} {x : X} {l : filter α} :
filter.tendsto (separation_quotient.lift f hf) (nhds (separation_quotient.mk x)) l ↔ filter.tendsto f (nhds x) l
source
@[simp]
theorem separation_quotient.tendsto_lift_nhds_within_mk {X : Type u_1} {α : Type u_4} [topological_space X] {f : X → α} {hf : ∀ (x y : X), inseparable x y → f x = f y} {x : X} {s : set (separation_quotient X)} {l : filter α} :
filter.tendsto (separation_quotient.lift f hf) (nhds_within (separation_quotient.mk x) s) l ↔ filter.tendsto f (nhds_within x (separation_quotient.mk ⁻¹' s)) l
source
@[simp]
theorem separation_quotient.continuous_at_lift {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] {f : X → Y} {hf : ∀ (x y : X), inseparable x y → f x = f y} {x : X} :
continuous_at (separation_quotient.lift f hf) (separation_quotient.mk x) ↔ continuous_at f x
source
@[simp]
theorem separation_quotient.continuous_within_at_lift {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] {f : X → Y} {hf : ∀ (x y : X), inseparable x y → f x = f y} {s : set (separation_quotient X)} {x : X} :
continuous_within_at (separation_quotient.lift f hf) s (separation_quotient.mk x) ↔ continuous_within_at f (separation_quotient.mk ⁻¹' s) x
source
@[simp]
theorem separation_quotient.continuous_on_lift {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] {f : X → Y} {hf : ∀ (x y : X), inseparable x y → f x = f y} {s : set (separation_quotient X)} :
continuous_on (separation_quotient.lift f hf) s ↔ continuous_on f (separation_quotient.mk ⁻¹' s)
source
@[simp]
theorem separation_quotient.continuous_lift {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] {f : X → Y} {hf : ∀ (x y : X), inseparable x y → f x = f y} :
continuous (separation_quotient.lift f hf) ↔ continuous f
source
def separation_quotient.lift₂ {X : Type u_1} {Y : Type u_2} {α : Type u_4} [topological_space X] [topological_space Y] (f : X → Y → α) (hf : ∀ (a : X) (b : Y) (c : X) (d : Y), inseparable a c → inseparable b d → f a b = f c d) :
separation_quotient X → separation_quotient Y → α

Lift a map f : X → Y → α such that inseparable a b → inseparable c d → f a c = f b d to a map separation_quotient X → separation_quotient Y → α.

Equations
source
@[simp]
theorem separation_quotient.lift₂_mk {X : Type u_1} {Y : Type u_2} {α : Type u_4} [topological_space X] [topological_space Y] {f : X → Y → α} (hf : ∀ (a : X) (b : Y) (c : X) (d : Y), inseparable a c → inseparable b d → f a b = f c d) (x : X) (y : Y) :
separation_quotient.lift₂ f hf (separation_quotient.mk x) (separation_quotient.mk y) = f x y
source
@[simp]
theorem separation_quotient.tendsto_lift₂_nhds {X : Type u_1} {Y : Type u_2} {α : Type u_4} [topological_space X] [topological_space Y] {f : X → Y → α} {hf : ∀ (a : X) (b : Y) (c : X) (d : Y), inseparable a c → inseparable b d → f a b = f c d} {x : X} {y : Y} {l : filter α} :
filter.tendsto (function.uncurry (separation_quotient.lift₂ f hf)) (nhds (separation_quotient.mk x, separation_quotient.mk y)) l ↔ filter.tendsto (function.uncurry f) (nhds (x, y)) l
source
@[simp]
theorem separation_quotient.tendsto_lift₂_nhds_within {X : Type u_1} {Y : Type u_2} {α : Type u_4} [topological_space X] [topological_space Y] {f : X → Y → α} {hf : ∀ (a : X) (b : Y) (c : X) (d : Y), inseparable a c → inseparable b d → f a b = f c d} {x : X} {y : Y} {s : set (separation_quotient X × separation_quotient Y)} {l : filter α} :
filter.tendsto (function.uncurry (separation_quotient.lift₂ f hf)) (nhds_within (separation_quotient.mk x, separation_quotient.mk y) s) l ↔ filter.tendsto (function.uncurry f) (nhds_within (x, y) (prod.map separation_quotient.mk separation_quotient.mk ⁻¹' s)) l
source
@[simp]
theorem separation_quotient.continuous_at_lift₂ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [topological_space X] [topological_space Y] [topological_space Z] {f : X → Y → Z} {hf : ∀ (a : X) (b : Y) (c : X) (d : Y), inseparable a c → inseparable b d → f a b = f c d} {x : X} {y : Y} :
continuous_at (function.uncurry (separation_quotient.lift₂ f hf)) (separation_quotient.mk x, separation_quotient.mk y) ↔ continuous_at (function.uncurry f) (x, y)
source
@[simp]
theorem separation_quotient.continuous_within_at_lift₂ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [topological_space X] [topological_space Y] [topological_space Z] {f : X → Y → Z} {hf : ∀ (a : X) (b : Y) (c : X) (d : Y), inseparable a c → inseparable b d → f a b = f c d} {s : set (separation_quotient X × separation_quotient Y)} {x : X} {y : Y} :
continuous_within_at (function.uncurry (separation_quotient.lift₂ f hf)) s (separation_quotient.mk x, separation_quotient.mk y) ↔ continuous_within_at (function.uncurry f) (prod.map separation_quotient.mk separation_quotient.mk ⁻¹' s) (x, y)
source
@[simp]
theorem separation_quotient.continuous_on_lift₂ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [topological_space X] [topological_space Y] [topological_space Z] {f : X → Y → Z} {hf : ∀ (a : X) (b : Y) (c : X) (d : Y), inseparable a c → inseparable b d → f a b = f c d} {s : set (separation_quotient X × separation_quotient Y)} :
continuous_on (function.uncurry (separation_quotient.lift₂ f hf)) s ↔ continuous_on (function.uncurry f) (prod.map separation_quotient.mk separation_quotient.mk ⁻¹' s)
source
@[simp]
theorem separation_quotient.continuous_lift₂ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [topological_space X] [topological_space Y] [topological_space Z] {f : X → Y → Z} {hf : ∀ (a : X) (b : Y) (c : X) (d : Y), inseparable a c → inseparable b d → f a b = f c d} :
continuous (function.uncurry (separation_quotient.lift₂ f hf)) ↔ continuous (function.uncurry f)