[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
t t' : Bornology α
h_cobounded : cobounded α = cobounded α
⊢ t = t'
[PROOFSTEP]
cases t
[GOAL]
case mk
ι : Type u_1
α : Type u_2
β : Type u_3
t' : Bornology α
cobounded'✝ : Filter α
le_cofinite'✝ : cobounded'✝ ≤ cofinite
h_cobounded : cobounded α = cobounded α
⊢ { cobounded' := cobounded'✝, le_cofinite' := le_cofinite'✝ } = t'
[PROOFSTEP]
cases t'
[GOAL]
case mk.mk
ι : Type u_1
α : Type u_2
β : Type u_3
cobounded'✝¹ : Filter α
le_cofinite'✝¹ : cobounded'✝¹ ≤ cofinite
cobounded'✝ : Filter α
le_cofinite'✝ : cobounded'✝ ≤ cofinite
h_cobounded : cobounded α = cobounded α
⊢ { cobounded' := cobounded'✝¹, le_cofinite' := le_cofinite'✝¹ } =
    { cobounded' := cobounded'✝, le_cofinite' := le_cofinite'✝ }
[PROOFSTEP]
congr
[GOAL]
ι : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type u_4
B : Set (Set α)
empty_mem : ∅ ∈ B
subset_mem : ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B
union_mem : ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B
singleton_mem : ∀ (x : α), {x} ∈ B
⊢ univ ∈ {s | sᶜ ∈ B}
[PROOFSTEP]
rwa [← compl_univ] at empty_mem
[GOAL]
ι : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type u_4
B : Set (Set α)
empty_mem : ∅ ∈ B
subset_mem : ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B
union_mem : ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B
singleton_mem : ∀ (x : α), {x} ∈ B
x✝ y✝ : Set α
hx : x✝ ∈ {s | sᶜ ∈ B}
hy : y✝ ∈ {s | sᶜ ∈ B}
⊢ x✝ ∩ y✝ ∈ {s | sᶜ ∈ B}
[PROOFSTEP]
simpa [compl_inter] using union_mem _ hx _ hy
[GOAL]
ι : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type u_4
B : Set (Set α)
empty_mem : ∅ ∈ B
subset_mem : ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B
union_mem : ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B
singleton_mem : ∀ (x : α), {x} ∈ B
⊢ { sets := {s | sᶜ ∈ B}, univ_sets := (_ : univᶜ ∈ B),
      sets_of_superset := (_ : ∀ {x y : Set α}, x ∈ {s | sᶜ ∈ B} → x ⊆ y → yᶜ ∈ B),
      inter_sets := (_ : ∀ {x y : Set α}, x ∈ {s | sᶜ ∈ B} → y ∈ {s | sᶜ ∈ B} → x ∩ y ∈ {s | sᶜ ∈ B}) } ≤
    cofinite
[PROOFSTEP]
rw [le_cofinite_iff_compl_singleton_mem]
[GOAL]
ι : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type u_4
B : Set (Set α)
empty_mem : ∅ ∈ B
subset_mem : ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B
union_mem : ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B
singleton_mem : ∀ (x : α), {x} ∈ B
⊢ ∀ (x : α),
    {x}ᶜ ∈
      { sets := {s | sᶜ ∈ B}, univ_sets := (_ : univᶜ ∈ B),
        sets_of_superset := (_ : ∀ {x y : Set α}, x ∈ {s | sᶜ ∈ B} → x ⊆ y → yᶜ ∈ B),
        inter_sets := (_ : ∀ {x y : Set α}, x ∈ {s | sᶜ ∈ B} → y ∈ {s | sᶜ ∈ B} → x ∩ y ∈ {s | sᶜ ∈ B}) }
[PROOFSTEP]
intro x
[GOAL]
ι : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type u_4
B : Set (Set α)
empty_mem : ∅ ∈ B
subset_mem : ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B
union_mem : ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B
singleton_mem : ∀ (x : α), {x} ∈ B
x : α
⊢ {x}ᶜ ∈
    { sets := {s | sᶜ ∈ B}, univ_sets := (_ : univᶜ ∈ B),
      sets_of_superset := (_ : ∀ {x y : Set α}, x ∈ {s | sᶜ ∈ B} → x ⊆ y → yᶜ ∈ B),
      inter_sets := (_ : ∀ {x y : Set α}, x ∈ {s | sᶜ ∈ B} → y ∈ {s | sᶜ ∈ B} → x ∩ y ∈ {s | sᶜ ∈ B}) }
[PROOFSTEP]
change { x }ᶜᶜ ∈ B
[GOAL]
ι : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type u_4
B : Set (Set α)
empty_mem : ∅ ∈ B
subset_mem : ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B
union_mem : ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B
singleton_mem : ∀ (x : α), {x} ∈ B
x : α
⊢ {x}ᶜᶜ ∈ B
[PROOFSTEP]
rw [compl_compl]
[GOAL]
ι : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type u_4
B : Set (Set α)
empty_mem : ∅ ∈ B
subset_mem : ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B
union_mem : ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B
singleton_mem : ∀ (x : α), {x} ∈ B
x : α
⊢ {x} ∈ B
[PROOFSTEP]
exact singleton_mem x
[GOAL]
ι : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type u_4
B : Set (Set α)
empty_mem : ∅ ∈ B
subset_mem : ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B
union_mem : ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B
sUnion_univ : ⋃₀ B = univ
x : α
⊢ {x} ∈ B
[PROOFSTEP]
rw [sUnion_eq_univ_iff] at sUnion_univ
[GOAL]
ι : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type u_4
B : Set (Set α)
empty_mem : ∅ ∈ B
subset_mem : ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B
union_mem : ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B
sUnion_univ : ∀ (a : α), ∃ b, b ∈ B ∧ a ∈ b
x : α
⊢ {x} ∈ B
[PROOFSTEP]
rcases sUnion_univ x with ⟨s, hs, hxs⟩
[GOAL]
case intro.intro
ι : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type u_4
B : Set (Set α)
empty_mem : ∅ ∈ B
subset_mem : ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B
union_mem : ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B
sUnion_univ : ∀ (a : α), ∃ b, b ∈ B ∧ a ∈ b
x : α
s : Set α
hs : s ∈ B
hxs : x ∈ s
⊢ {x} ∈ B
[PROOFSTEP]
exact subset_mem s hs { x } (singleton_subset_iff.mpr hxs)
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : Bornology α
s t : Set α
x : α
⊢ IsBounded sᶜ ↔ IsCobounded s
[PROOFSTEP]
rw [isBounded_def, isCobounded_def, compl_compl]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : Bornology α
s t : Set α
x : α
⊢ IsBounded ∅
[PROOFSTEP]
rw [isBounded_def, compl_empty]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : Bornology α
s t : Set α
x : α
⊢ univ ∈ cobounded α
[PROOFSTEP]
exact univ_mem
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : Bornology α
s t : Set α
x : α
⊢ IsBounded {x}
[PROOFSTEP]
rw [isBounded_def]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : Bornology α
s t : Set α
x : α
⊢ {x}ᶜ ∈ cobounded α
[PROOFSTEP]
exact le_cofinite _ (finite_singleton x).compl_mem_cofinite
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : Bornology α
s t : Set α
x : α
⊢ IsBounded (s ∪ t) ↔ IsBounded s ∧ IsBounded t
[PROOFSTEP]
simp only [← isCobounded_compl_iff, compl_union, isCobounded_inter]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : Bornology α
s t : Set α
x : α
inst✝ : Bornology β
f : α → β
⊢ comap f (cobounded β) ≤ cobounded α ↔ ∀ ⦃s : Set α⦄, IsBounded s → IsBounded (f '' s)
[PROOFSTEP]
refine'
  ⟨fun h s hs => _, fun h t ht =>
    ⟨(f '' tᶜ)ᶜ, h <| IsCobounded.compl ht, compl_subset_comm.1 <| subset_preimage_image _ _⟩⟩
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : Bornology α
s✝ t : Set α
x : α
inst✝ : Bornology β
f : α → β
h : comap f (cobounded β) ≤ cobounded α
s : Set α
hs : IsBounded s
⊢ IsBounded (f '' s)
[PROOFSTEP]
obtain ⟨t, ht, hts⟩ := h hs.compl
[GOAL]
case intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : Bornology α
s✝ t✝ : Set α
x : α
inst✝ : Bornology β
f : α → β
h : comap f (cobounded β) ≤ cobounded α
s : Set α
hs : IsBounded s
t : Set β
ht : t ∈ cobounded β
hts : f ⁻¹' t ⊆ sᶜ
⊢ IsBounded (f '' s)
[PROOFSTEP]
rw [subset_compl_comm, ← preimage_compl] at hts
[GOAL]
case intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : Bornology α
s✝ t✝ : Set α
x : α
inst✝ : Bornology β
f : α → β
h : comap f (cobounded β) ≤ cobounded α
s : Set α
hs : IsBounded s
t : Set β
ht : t ∈ cobounded β
hts : s ⊆ f ⁻¹' tᶜ
⊢ IsBounded (f '' s)
[PROOFSTEP]
exact (IsCobounded.compl ht).subset ((image_subset f hts).trans <| image_preimage_subset _ _)
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
t t' : Bornology α
h : ∀ (s : Set α), IsBounded s ↔ IsBounded s
⊢ t = t'
[PROOFSTEP]
ext s
[GOAL]
case h_cobounded.a
ι : Type u_1
α : Type u_2
β : Type u_3
t t' : Bornology α
h : ∀ (s : Set α), IsBounded s ↔ IsBounded s
s : Set α
⊢ s ∈ cobounded α ↔ s ∈ cobounded α
[PROOFSTEP]
simpa [@isBounded_def _ t, isBounded_def, compl_compl] using h sᶜ
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
s : Set α
B : Set (Set α)
empty_mem : ∅ ∈ B
subset_mem : ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B
union_mem : ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B
sUnion_univ : ∀ (x : α), {x} ∈ B
⊢ IsBounded s ↔ s ∈ B
[PROOFSTEP]
rw [@isBounded_def _ (ofBounded B empty_mem subset_mem union_mem sUnion_univ), ← Filter.mem_sets,
  ofBounded_cobounded_sets, Set.mem_setOf_eq, compl_compl]
  -- porting note: again had to use `@isBounded_def _` and feed Lean the instance
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
s✝ : Set α
inst✝ : Bornology α
s : Set ι
f : ι → Set α
hs : Set.Finite s
⊢ IsBounded (⋃ (i : ι) (_ : i ∈ s), f i) ↔ ∀ (i : ι), i ∈ s → IsBounded (f i)
[PROOFSTEP]
simp only [← isCobounded_compl_iff, compl_iUnion, isCobounded_biInter hs]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
s : Set α
inst✝ : Bornology α
S : Set (Set α)
hs : Set.Finite S
⊢ IsBounded (⋃₀ S) ↔ ∀ (s : Set α), s ∈ S → IsBounded s
[PROOFSTEP]
rw [sUnion_eq_biUnion, isBounded_biUnion hs]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
s✝ : Set α
inst✝¹ : Bornology α
inst✝ : Finite ι
s : ι → Set α
⊢ IsBounded (⋃ (i : ι), s i) ↔ ∀ (i : ι), IsBounded (s i)
[PROOFSTEP]
rw [← sUnion_range, isBounded_sUnion (finite_range s), forall_range_iff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : Bornology α
⊢ cobounded α = ⊥ ↔ BoundedSpace α
[PROOFSTEP]
rw [← isBounded_univ, isBounded_def, compl_univ, empty_mem_iff_bot]


[GOAL]
α : Type u_1
inst✝² : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝¹ : UniformSpace β
f : α → β
inst✝ : T2Space β
hf : UniformContinuous f
a : α
⊢ AbstractCompletion.extend pkg f (coe pkg a) = f a
[PROOFSTEP]
rw [pkg.extend_def hf]
[GOAL]
α : Type u_1
inst✝² : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝¹ : UniformSpace β
f : α → β
inst✝ : T2Space β
hf : UniformContinuous f
a : α
⊢ DenseInducing.extend (_ : DenseInducing pkg.coe) f (coe pkg a) = f a
[PROOFSTEP]
exact pkg.denseInducing.extend_eq hf.continuous a
[GOAL]
α : Type u_1
inst✝² : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝¹ : UniformSpace β
f : α → β
inst✝ : CompleteSpace β
⊢ UniformContinuous (AbstractCompletion.extend pkg f)
[PROOFSTEP]
by_cases hf : UniformContinuous f
[GOAL]
case pos
α : Type u_1
inst✝² : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝¹ : UniformSpace β
f : α → β
inst✝ : CompleteSpace β
hf : UniformContinuous f
⊢ UniformContinuous (AbstractCompletion.extend pkg f)
[PROOFSTEP]
rw [pkg.extend_def hf]
[GOAL]
case pos
α : Type u_1
inst✝² : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝¹ : UniformSpace β
f : α → β
inst✝ : CompleteSpace β
hf : UniformContinuous f
⊢ UniformContinuous (DenseInducing.extend (_ : DenseInducing pkg.coe) f)
[PROOFSTEP]
exact uniformContinuous_uniformly_extend pkg.uniformInducing pkg.dense hf
[GOAL]
case neg
α : Type u_1
inst✝² : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝¹ : UniformSpace β
f : α → β
inst✝ : CompleteSpace β
hf : ¬UniformContinuous f
⊢ UniformContinuous (AbstractCompletion.extend pkg f)
[PROOFSTEP]
change UniformContinuous (ite _ _ _)
[GOAL]
case neg
α : Type u_1
inst✝² : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝¹ : UniformSpace β
f : α → β
inst✝ : CompleteSpace β
hf : ¬UniformContinuous f
⊢ UniformContinuous
    (if UniformContinuous f then DenseInducing.extend (_ : DenseInducing pkg.coe) f
    else fun x => f (DenseRange.some (_ : DenseRange pkg.coe) x))
[PROOFSTEP]
rw [if_neg hf]
[GOAL]
case neg
α : Type u_1
inst✝² : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝¹ : UniformSpace β
f : α → β
inst✝ : CompleteSpace β
hf : ¬UniformContinuous f
⊢ UniformContinuous fun x => f (DenseRange.some (_ : DenseRange pkg.coe) x)
[PROOFSTEP]
exact uniformContinuous_of_const fun a b => by congr 1
[GOAL]
α : Type u_1
inst✝² : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝¹ : UniformSpace β
f : α → β
inst✝ : CompleteSpace β
hf : ¬UniformContinuous f
a b : pkg.space
⊢ f (DenseRange.some (_ : DenseRange pkg.coe) a) = f (DenseRange.some (_ : DenseRange pkg.coe) b)
[PROOFSTEP]
congr 1
[GOAL]
α : Type u_1
inst✝³ : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝² : UniformSpace β
f : α → β
inst✝¹ : CompleteSpace β
inst✝ : SeparatedSpace β
hf : UniformContinuous f
g : pkg.space → β
hg : UniformContinuous g
h : ∀ (a : α), f a = g (coe pkg a)
⊢ AbstractCompletion.extend pkg f = g
[PROOFSTEP]
apply pkg.funext pkg.continuous_extend hg.continuous
[GOAL]
α : Type u_1
inst✝³ : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝² : UniformSpace β
f : α → β
inst✝¹ : CompleteSpace β
inst✝ : SeparatedSpace β
hf : UniformContinuous f
g : pkg.space → β
hg : UniformContinuous g
h : ∀ (a : α), f a = g (coe pkg a)
⊢ ∀ (a : α), AbstractCompletion.extend pkg f (coe pkg a) = g (coe pkg a)
[PROOFSTEP]
simpa only [pkg.extend_coe hf] using h
[GOAL]
α : Type u_1
inst✝¹ : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝ : UniformSpace β
pkg' : AbstractCompletion β
f✝ f : α → β
g : pkg.space → pkg'.space
hg : UniformContinuous g
h : ∀ (a : α), coe pkg' (f a) = g (coe pkg a)
⊢ ∀ (a : α), AbstractCompletion.map pkg pkg' f (coe pkg a) = g (coe pkg a)
[PROOFSTEP]
intro a
[GOAL]
α : Type u_1
inst✝¹ : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝ : UniformSpace β
pkg' : AbstractCompletion β
f✝ f : α → β
g : pkg.space → pkg'.space
hg : UniformContinuous g
h : ∀ (a : α), coe pkg' (f a) = g (coe pkg a)
a : α
⊢ AbstractCompletion.map pkg pkg' f (coe pkg a) = g (coe pkg a)
[PROOFSTEP]
change pkg.extend (ι' ∘ f) _ = _
[GOAL]
α : Type u_1
inst✝¹ : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝ : UniformSpace β
pkg' : AbstractCompletion β
f✝ f : α → β
g : pkg.space → pkg'.space
hg : UniformContinuous g
h : ∀ (a : α), coe pkg' (f a) = g (coe pkg a)
a : α
⊢ AbstractCompletion.extend pkg (pkg'.coe ∘ f) (coe pkg a) = g (coe pkg a)
[PROOFSTEP]
simp only [(· ∘ ·), h, ← comp_apply (f := g)]
[GOAL]
α : Type u_1
inst✝¹ : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝ : UniformSpace β
pkg' : AbstractCompletion β
f✝ f : α → β
g : pkg.space → pkg'.space
hg : UniformContinuous g
h : ∀ (a : α), coe pkg' (f a) = g (coe pkg a)
a : α
⊢ AbstractCompletion.extend pkg (fun x => (g ∘ pkg.coe) x) (coe pkg a) = (g ∘ pkg.coe) a
[PROOFSTEP]
rw [pkg.extend_coe (hg.comp pkg.uniformContinuous_coe)]
[GOAL]
α : Type u_1
inst✝⁴ : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝³ : UniformSpace β
pkg' : AbstractCompletion β
f✝ : α → β
γ : Type u_3
inst✝² : UniformSpace γ
inst✝¹ : CompleteSpace γ
inst✝ : SeparatedSpace γ
f : β → γ
g : α → β
hf : UniformContinuous f
hg : UniformContinuous g
a : α
⊢ (AbstractCompletion.extend pkg' f ∘ AbstractCompletion.map pkg pkg' g) (coe pkg a) =
    AbstractCompletion.extend pkg (f ∘ g) (coe pkg a)
[PROOFSTEP]
rw [pkg.extend_coe (hf.comp hg), comp_apply, pkg.map_coe pkg' hg, pkg'.extend_coe hf]
[GOAL]
α : Type u_1
inst✝⁴ : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝³ : UniformSpace β
pkg' : AbstractCompletion β
f✝ : α → β
γ : Type u_3
inst✝² : UniformSpace γ
inst✝¹ : CompleteSpace γ
inst✝ : SeparatedSpace γ
f : β → γ
g : α → β
hf : UniformContinuous f
hg : UniformContinuous g
a : α
⊢ f (g a) = (f ∘ g) a
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝¹ : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝ : UniformSpace β
pkg' : AbstractCompletion α
⊢ compare pkg pkg' ∘ compare pkg' pkg = id
[PROOFSTEP]
have uc := pkg.uniformContinuous_compare pkg'
[GOAL]
α : Type u_1
inst✝¹ : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝ : UniformSpace β
pkg' : AbstractCompletion α
uc : UniformContinuous (compare pkg pkg')
⊢ compare pkg pkg' ∘ compare pkg' pkg = id
[PROOFSTEP]
have uc' := pkg'.uniformContinuous_compare pkg
[GOAL]
α : Type u_1
inst✝¹ : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝ : UniformSpace β
pkg' : AbstractCompletion α
uc : UniformContinuous (compare pkg pkg')
uc' : UniformContinuous (compare pkg' pkg)
⊢ compare pkg pkg' ∘ compare pkg' pkg = id
[PROOFSTEP]
apply pkg'.funext (uc.comp uc').continuous continuous_id
[GOAL]
α : Type u_1
inst✝¹ : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝ : UniformSpace β
pkg' : AbstractCompletion α
uc : UniformContinuous (compare pkg pkg')
uc' : UniformContinuous (compare pkg' pkg)
⊢ ∀ (a : α), (compare pkg pkg' ∘ compare pkg' pkg) (coe pkg' a) = id (coe pkg' a)
[PROOFSTEP]
intro a
[GOAL]
α : Type u_1
inst✝¹ : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝ : UniformSpace β
pkg' : AbstractCompletion α
uc : UniformContinuous (compare pkg pkg')
uc' : UniformContinuous (compare pkg' pkg)
a : α
⊢ (compare pkg pkg' ∘ compare pkg' pkg) (coe pkg' a) = id (coe pkg' a)
[PROOFSTEP]
rw [comp_apply, pkg'.compare_coe pkg, pkg.compare_coe pkg']
[GOAL]
α : Type u_1
inst✝¹ : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝ : UniformSpace β
pkg' : AbstractCompletion α
uc : UniformContinuous (compare pkg pkg')
uc' : UniformContinuous (compare pkg' pkg)
a : α
⊢ coe pkg' a = id (coe pkg' a)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝³ : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝² : UniformSpace β
pkg' : AbstractCompletion β
γ : Type u_3
inst✝¹ : UniformSpace γ
f : α → β → γ
inst✝ : CompleteSpace γ
⊢ UniformContinuous₂ (AbstractCompletion.extend₂ pkg pkg' f)
[PROOFSTEP]
rw [uniformContinuous₂_def, AbstractCompletion.extend₂, uncurry_curry]
[GOAL]
α : Type u_1
inst✝³ : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝² : UniformSpace β
pkg' : AbstractCompletion β
γ : Type u_3
inst✝¹ : UniformSpace γ
f : α → β → γ
inst✝ : CompleteSpace γ
⊢ UniformContinuous (AbstractCompletion.extend (AbstractCompletion.prod pkg pkg') (uncurry f))
[PROOFSTEP]
apply uniformContinuous_extend


[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝³ : Fintype ι
inst✝² : Bornology α
inst✝¹ : Bornology β
inst✝ : (i : ι) → Bornology (π i)
s : Set α
t : Set β
S : (i : ι) → Set (π i)
⊢ IsBounded (s ×ˢ t) ↔ s = ∅ ∨ t = ∅ ∨ IsBounded s ∧ IsBounded t
[PROOFSTEP]
rcases s.eq_empty_or_nonempty with (rfl | hs)
[GOAL]
case inl
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝³ : Fintype ι
inst✝² : Bornology α
inst✝¹ : Bornology β
inst✝ : (i : ι) → Bornology (π i)
t : Set β
S : (i : ι) → Set (π i)
⊢ IsBounded (∅ ×ˢ t) ↔ ∅ = ∅ ∨ t = ∅ ∨ IsBounded ∅ ∧ IsBounded t
[PROOFSTEP]
simp
[GOAL]
case inr
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝³ : Fintype ι
inst✝² : Bornology α
inst✝¹ : Bornology β
inst✝ : (i : ι) → Bornology (π i)
s : Set α
t : Set β
S : (i : ι) → Set (π i)
hs : Set.Nonempty s
⊢ IsBounded (s ×ˢ t) ↔ s = ∅ ∨ t = ∅ ∨ IsBounded s ∧ IsBounded t
[PROOFSTEP]
rcases t.eq_empty_or_nonempty with (rfl | ht)
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝³ : Fintype ι
inst✝² : Bornology α
inst✝¹ : Bornology β
inst✝ : (i : ι) → Bornology (π i)
s : Set α
S : (i : ι) → Set (π i)
hs : Set.Nonempty s
⊢ IsBounded (s ×ˢ ∅) ↔ s = ∅ ∨ ∅ = ∅ ∨ IsBounded s ∧ IsBounded ∅
[PROOFSTEP]
simp
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝³ : Fintype ι
inst✝² : Bornology α
inst✝¹ : Bornology β
inst✝ : (i : ι) → Bornology (π i)
s : Set α
t : Set β
S : (i : ι) → Set (π i)
hs : Set.Nonempty s
ht : Set.Nonempty t
⊢ IsBounded (s ×ˢ t) ↔ s = ∅ ∨ t = ∅ ∨ IsBounded s ∧ IsBounded t
[PROOFSTEP]
simp only [hs.ne_empty, ht.ne_empty, isBounded_prod_of_nonempty (hs.prod ht), false_or_iff]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝³ : Fintype ι
inst✝² : Bornology α
inst✝¹ : Bornology β
inst✝ : (i : ι) → Bornology (π i)
s : Set α
t : Set β
S : (i : ι) → Set (π i)
⊢ IsBounded (s ×ˢ s) ↔ IsBounded s
[PROOFSTEP]
rcases s.eq_empty_or_nonempty with (rfl | hs)
[GOAL]
case inl
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝³ : Fintype ι
inst✝² : Bornology α
inst✝¹ : Bornology β
inst✝ : (i : ι) → Bornology (π i)
t : Set β
S : (i : ι) → Set (π i)
⊢ IsBounded (∅ ×ˢ ∅) ↔ IsBounded ∅
[PROOFSTEP]
simp
[GOAL]
case inr
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝³ : Fintype ι
inst✝² : Bornology α
inst✝¹ : Bornology β
inst✝ : (i : ι) → Bornology (π i)
s : Set α
t : Set β
S : (i : ι) → Set (π i)
hs : Set.Nonempty s
⊢ IsBounded (s ×ˢ s) ↔ IsBounded s
[PROOFSTEP]
exact (isBounded_prod_of_nonempty (hs.prod hs)).trans (and_self_iff _)
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝³ : Fintype ι
inst✝² : Bornology α
inst✝¹ : Bornology β
inst✝ : (i : ι) → Bornology (π i)
s : Set α
t : Set β
S : (i : ι) → Set (π i)
⊢ IsBounded (Set.pi univ S) ↔ (∃ i, S i = ∅) ∨ ∀ (i : ι), IsBounded (S i)
[PROOFSTEP]
by_cases hne : ∃ i, S i = ∅
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝³ : Fintype ι
inst✝² : Bornology α
inst✝¹ : Bornology β
inst✝ : (i : ι) → Bornology (π i)
s : Set α
t : Set β
S : (i : ι) → Set (π i)
hne : ∃ i, S i = ∅
⊢ IsBounded (Set.pi univ S) ↔ (∃ i, S i = ∅) ∨ ∀ (i : ι), IsBounded (S i)
[PROOFSTEP]
simp [hne, univ_pi_eq_empty_iff.2 hne]
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝³ : Fintype ι
inst✝² : Bornology α
inst✝¹ : Bornology β
inst✝ : (i : ι) → Bornology (π i)
s : Set α
t : Set β
S : (i : ι) → Set (π i)
hne : ¬∃ i, S i = ∅
⊢ IsBounded (Set.pi univ S) ↔ (∃ i, S i = ∅) ∨ ∀ (i : ι), IsBounded (S i)
[PROOFSTEP]
simp only [hne, false_or_iff]
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝³ : Fintype ι
inst✝² : Bornology α
inst✝¹ : Bornology β
inst✝ : (i : ι) → Bornology (π i)
s : Set α
t : Set β
S : (i : ι) → Set (π i)
hne : ¬∃ i, S i = ∅
⊢ IsBounded (Set.pi univ S) ↔ ∀ (i : ι), IsBounded (S i)
[PROOFSTEP]
simp only [not_exists, ← Ne.def, ← nonempty_iff_ne_empty, ← univ_pi_nonempty_iff] at hne
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝³ : Fintype ι
inst✝² : Bornology α
inst✝¹ : Bornology β
inst✝ : (i : ι) → Bornology (π i)
s : Set α
t : Set β
S : (i : ι) → Set (π i)
hne : Set.Nonempty (Set.pi univ fun i => S i)
⊢ IsBounded (Set.pi univ S) ↔ ∀ (i : ι), IsBounded (S i)
[PROOFSTEP]
exact isBounded_pi_of_nonempty hne
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : Bornology α
inst✝³ : Bornology β
inst✝² : (i : ι) → Bornology (π i)
inst✝¹ : BoundedSpace α
inst✝ : BoundedSpace β
⊢ BoundedSpace (α × β)
[PROOFSTEP]
simp [← cobounded_eq_bot_iff, cobounded_prod]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝⁴ : Fintype ι
inst✝³ : Bornology α
inst✝² : Bornology β
inst✝¹ : (i : ι) → Bornology (π i)
inst✝ : ∀ (i : ι), BoundedSpace (π i)
⊢ BoundedSpace ((i : ι) → π i)
[PROOFSTEP]
simp [← cobounded_eq_bot_iff, cobounded_pi]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝⁴ : Fintype ι
inst✝³ : Bornology α✝
inst✝² : Bornology β✝
inst✝¹ : (i : ι) → Bornology (π i)
α : Type u_5
β : Type u_6
inst✝ : Bornology β
f : α → β
⊢ BoundedSpace α ↔ IsBounded (range f)
[PROOFSTEP]
rw [← @isBounded_univ _ (Bornology.induced f), isBounded_induced, image_univ]
  -- porting note: had to explicitly provided the bornology to `isBounded_univ`.
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝³ : Fintype ι
inst✝² : Bornology α
inst✝¹ : Bornology β
inst✝ : (i : ι) → Bornology (π i)
p : α → Prop
⊢ BoundedSpace (Subtype p) ↔ IsBounded {x | p x}
[PROOFSTEP]
rw [boundedSpace_induced_iff, Subtype.range_coe_subtype]


[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
⊢ UniformInducing f ↔ UniformContinuous f ∧ comap (Prod.map f f) (𝓤 β) ≤ 𝓤 α
[PROOFSTEP]
rw [uniformInducing_iff, UniformContinuous, tendsto_iff_comap, le_antisymm_iff, and_comm]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
⊢ 𝓤 α ≤ comap (fun x => (f x.fst, f x.snd)) (𝓤 β) ∧ comap (fun x => (f x.fst, f x.snd)) (𝓤 β) ≤ 𝓤 α ↔
    𝓤 α ≤ comap (fun x => (f x.fst, f x.snd)) (𝓤 β) ∧ comap (Prod.map f f) (𝓤 β) ≤ 𝓤 α
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
ι : Sort u_1
ι' : Sort u_2
p : ι → Prop
p' : ι' → Prop
s : ι → Set (α × α)
s' : ι' → Set (β × β)
h : HasBasis (𝓤 α) p s
h' : HasBasis (𝓤 β) p' s'
f : α → β
⊢ UniformInducing f ↔
    (∀ (i : ι'), p' i → ∃ j, p j ∧ ∀ (x y : α), (x, y) ∈ s j → (f x, f y) ∈ s' i) ∧
      ∀ (j : ι), p j → ∃ i, p' i ∧ ∀ (x y : α), (f x, f y) ∈ s' i → (x, y) ∈ s j
[PROOFSTEP]
simp [uniformInducing_iff', h.uniformContinuous_iff h', (h'.comap _).le_basis_iff h, subset_def]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
h : ∀ (s : Set (α × α)), s ∈ 𝓤 α ↔ ∃ t, t ∈ 𝓤 β ∧ ∀ (x y : α), (f x, f y) ∈ t → (x, y) ∈ s
⊢ comap (fun x => (f x.fst, f x.snd)) (𝓤 β) = 𝓤 α
[PROOFSTEP]
simp [eq_comm, Filter.ext_iff, subset_def, h]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ comap (fun x => (id x.fst, id x.snd)) (𝓤 α) = 𝓤 α
[PROOFSTEP]
rw [← Prod.map_def, Prod.map_id, comap_id]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
g : β → γ
hg : UniformInducing g
f : α → β
hf : UniformInducing f
⊢ comap (fun x => ((g ∘ f) x.fst, (g ∘ f) x.snd)) (𝓤 γ) = 𝓤 α
[PROOFSTEP]
rw [← hf.1, ← hg.1, comap_comap]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
g : β → γ
hg : UniformInducing g
f : α → β
hf : UniformInducing f
⊢ comap (fun x => ((g ∘ f) x.fst, (g ∘ f) x.snd)) (𝓤 γ) =
    comap ((fun x => (g x.fst, g x.snd)) ∘ fun x => (f x.fst, f x.snd)) (𝓤 γ)
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
hf : UniformInducing f
F : Filter α
⊢ Cauchy (map f F) ↔ Cauchy F
[PROOFSTEP]
simp only [Cauchy, map_neBot_iff, prod_map_map_eq, map_le_iff_le_comap, ← hf.comap_uniformity]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
g : β → γ
hf : UniformContinuous f
hg : UniformContinuous g
hgf : UniformInducing (g ∘ f)
⊢ UniformInducing f
[PROOFSTEP]
refine' ⟨le_antisymm _ hf.le_comap⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
g : β → γ
hf : UniformContinuous f
hg : UniformContinuous g
hgf : UniformInducing (g ∘ f)
⊢ comap (fun x => (f x.fst, f x.snd)) (𝓤 β) ≤ 𝓤 α
[PROOFSTEP]
rw [← hgf.1, ← Prod.map_def, ← Prod.map_def, ← Prod.map_comp_map f f g g, ← comap_comap]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
g : β → γ
hf : UniformContinuous f
hg : UniformContinuous g
hgf : UniformInducing (g ∘ f)
⊢ comap (Prod.map f f) (𝓤 β) ≤ comap (Prod.map f f) (comap (Prod.map g g) (𝓤 γ))
[PROOFSTEP]
exact comap_mono hg.le_comap
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
g : β → γ
hg : UniformInducing g
⊢ UniformContinuous f ↔ UniformContinuous (g ∘ f)
[PROOFSTEP]
dsimp only [UniformContinuous, Tendsto]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
g : β → γ
hg : UniformInducing g
⊢ map (fun x => (f x.fst, f x.snd)) (𝓤 α) ≤ 𝓤 β ↔ map (fun x => ((g ∘ f) x.fst, (g ∘ f) x.snd)) (𝓤 α) ≤ 𝓤 γ
[PROOFSTEP]
rw [← hg.comap_uniformity, ← map_le_iff_le_comap, Filter.map_map]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
g : β → γ
hg : UniformInducing g
⊢ map ((fun x => (g x.fst, g x.snd)) ∘ fun x => (f x.fst, f x.snd)) (𝓤 α) ≤ 𝓤 γ ↔
    map (fun x => ((g ∘ f) x.fst, (g ∘ f) x.snd)) (𝓤 α) ≤ 𝓤 γ
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
h : UniformInducing f
⊢ Inducing f
[PROOFSTEP]
obtain rfl := h.comap_uniformSpace
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
h : UniformInducing f
⊢ Inducing f
[PROOFSTEP]
exact inducing_induced f
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : UniformSpace γ
α' : Type u_1
β' : Type u_2
inst✝¹ : UniformSpace α'
inst✝ : UniformSpace β'
e₁ : α → α'
e₂ : β → β'
h₁ : UniformInducing e₁
h₂ : UniformInducing e₂
⊢ comap (fun x => ((e₁ x.fst.fst, e₂ x.fst.snd), e₁ x.snd.fst, e₂ x.snd.snd)) (𝓤 (α' × β')) = 𝓤 (α × β)
[PROOFSTEP]
simp [(· ∘ ·), uniformity_prod, ← h₁.1, ← h₂.1, comap_inf, comap_comap]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
⊢ UniformEmbedding f ↔ Injective f ∧ UniformContinuous f ∧ comap (Prod.map f f) (𝓤 β) ≤ 𝓤 α
[PROOFSTEP]
rw [uniformEmbedding_iff, and_comm, uniformInducing_iff']
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
ι : Sort u_1
ι' : Sort u_2
p : ι → Prop
p' : ι' → Prop
s : ι → Set (α × α)
s' : ι' → Set (β × β)
h : HasBasis (𝓤 α) p s
h' : HasBasis (𝓤 β) p' s'
f : α → β
⊢ UniformEmbedding f ↔
    Injective f ∧
      (∀ (i : ι'), p' i → ∃ j, p j ∧ ∀ (x y : α), (x, y) ∈ s j → (f x, f y) ∈ s' i) ∧
        ∀ (j : ι), p j → ∃ i, p' i ∧ ∀ (x y : α), (f x, f y) ∈ s' i → (x, y) ∈ s j
[PROOFSTEP]
rw [uniformEmbedding_iff, and_comm, h.uniformInducing_iff h']
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
ι : Sort u_1
ι' : Sort u_2
p : ι → Prop
p' : ι' → Prop
s : ι → Set (α × α)
s' : ι' → Set (β × β)
h : HasBasis (𝓤 α) p s
h' : HasBasis (𝓤 β) p' s'
f : α → β
⊢ UniformEmbedding f ↔
    Injective f ∧ UniformContinuous f ∧ ∀ (j : ι), p j → ∃ i, p' i ∧ ∀ (x y : α), (f x, f y) ∈ s' i → (x, y) ∈ s j
[PROOFSTEP]
simp only [h.uniformEmbedding_iff' h', h.uniformContinuous_iff h']
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
s t : Set α
hst : s ⊆ t
⊢ comap (fun x => (inclusion hst x.fst, inclusion hst x.snd)) (𝓤 ↑t) = 𝓤 ↑s
[PROOFSTEP]
rw [uniformity_subtype, uniformity_subtype, comap_comap]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
s t : Set α
hst : s ⊆ t
⊢ comap ((fun q => (↑q.fst, ↑q.snd)) ∘ fun x => (inclusion hst x.fst, inclusion hst x.snd)) (𝓤 α) =
    comap (fun q => (↑q.fst, ↑q.snd)) (𝓤 α)
[PROOFSTEP]
rfl
[GOAL]
α✝ : Type u
β✝ : Type v
γ : Type w
inst✝⁴ : UniformSpace α✝
inst✝³ : UniformSpace β✝
inst✝² : UniformSpace γ
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α ≃ β
h₁ : UniformContinuous ↑f
h₂ : UniformContinuous ↑f.symm
⊢ comap (Prod.map ↑f ↑f) (𝓤 β) ≤ 𝓤 α
[PROOFSTEP]
rwa [← Equiv.prodCongr_apply, ← map_equiv_symm]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
s : Set (α × α)
hs : s ∈ 𝓤 α
x : α × α
h : x ∈ Prod.map Sum.inl Sum.inl ⁻¹' (Prod.map Sum.inl Sum.inl '' s ∪ range (Prod.map Sum.inr Sum.inr))
⊢ x ∈ s
[PROOFSTEP]
simpa using h
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
s : Set (β × β)
hs : s ∈ 𝓤 β
x : β × β
h : x ∈ Prod.map Sum.inr Sum.inr ⁻¹' (range (Prod.map Sum.inl Sum.inl) ∪ Prod.map Sum.inr Sum.inr '' s)
⊢ x ∈ s
[PROOFSTEP]
simpa using h
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α✝
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
α : Type u_1
f : α → β
s : Set (β × β)
hs : s ∈ 𝓤 β
hf : Pairwise fun x y => ¬(f x, f y) ∈ s
⊢ comap (Prod.map f f) (𝓤 β) = 𝓟 idRel
[PROOFSTEP]
refine' le_antisymm _ (@refl_le_uniformity α (UniformSpace.comap f _))
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α✝
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
α : Type u_1
f : α → β
s : Set (β × β)
hs : s ∈ 𝓤 β
hf : Pairwise fun x y => ¬(f x, f y) ∈ s
⊢ comap (Prod.map f f) (𝓤 β) ≤ 𝓟 idRel
[PROOFSTEP]
calc
  comap (Prod.map f f) (𝓤 β) ≤ comap (Prod.map f f) (𝓟 s) := comap_mono (le_principal_iff.2 hs)
  _ = 𝓟 (Prod.map f f ⁻¹' s) := comap_principal
  _ ≤ 𝓟 idRel := principal_mono.2 ?_
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α✝
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
α : Type u_1
f : α → β
s : Set (β × β)
hs : s ∈ 𝓤 β
hf : Pairwise fun x y => ¬(f x, f y) ∈ s
⊢ Prod.map f f ⁻¹' s ⊆ idRel
[PROOFSTEP]
rintro ⟨x, y⟩
[GOAL]
case mk
α✝ : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α✝
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
α : Type u_1
f : α → β
s : Set (β × β)
hs : s ∈ 𝓤 β
hf : Pairwise fun x y => ¬(f x, f y) ∈ s
x y : α
⊢ (x, y) ∈ Prod.map f f ⁻¹' s → (x, y) ∈ idRel
[PROOFSTEP]
simpa [not_imp_not] using @hf x y
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α✝
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
α : Type u_1
f : α → β
s : Set (β × β)
hs : s ∈ 𝓤 β
hf : Pairwise fun x y => ¬(f x, f y) ∈ s
⊢ UniformEmbedding f
[PROOFSTEP]
let _ : UniformSpace α := ⊥
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α✝
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
α : Type u_1
f : α → β
s : Set (β × β)
hs : s ∈ 𝓤 β
hf : Pairwise fun x y => ¬(f x, f y) ∈ s
x✝ : UniformSpace α := ⊥
⊢ UniformEmbedding f
[PROOFSTEP]
have := discreteTopology_bot α
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α✝
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
α : Type u_1
f : α → β
s : Set (β × β)
hs : s ∈ 𝓤 β
hf : Pairwise fun x y => ¬(f x, f y) ∈ s
x✝ : UniformSpace α := ⊥
this : DiscreteTopology α
⊢ UniformEmbedding f
[PROOFSTEP]
exact UniformInducing.uniformEmbedding ⟨comap_uniformity_of_spaced_out hs hf⟩
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
inst✝⁵ : UniformSpace α✝
inst✝⁴ : UniformSpace β
inst✝³ : UniformSpace γ
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : DiscreteTopology α
inst✝ : SeparatedSpace β
f : α → β
s : Set (β × β)
hs : s ∈ 𝓤 β
hf : Pairwise fun x y => ¬(f x, f y) ∈ s
⊢ ClosedEmbedding f
[PROOFSTEP]
rcases@DiscreteTopology.eq_bot α _ _ with rfl
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
inst✝⁴ : UniformSpace α✝
inst✝³ : UniformSpace β
inst✝² : UniformSpace γ
α : Type u_1
inst✝¹ : SeparatedSpace β
f : α → β
s : Set (β × β)
hs : s ∈ 𝓤 β
hf : Pairwise fun x y => ¬(f x, f y) ∈ s
inst✝ : DiscreteTopology α
⊢ ClosedEmbedding f
[PROOFSTEP]
let _ : UniformSpace α := ⊥
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
inst✝⁴ : UniformSpace α✝
inst✝³ : UniformSpace β
inst✝² : UniformSpace γ
α : Type u_1
inst✝¹ : SeparatedSpace β
f : α → β
s : Set (β × β)
hs : s ∈ 𝓤 β
hf : Pairwise fun x y => ¬(f x, f y) ∈ s
inst✝ : DiscreteTopology α
x✝ : UniformSpace α := ⊥
⊢ ClosedEmbedding f
[PROOFSTEP]
exact { (uniformEmbedding_of_spaced_out hs hf).embedding with closed_range := isClosed_range_of_spaced_out hs hf }
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
s : Set (α × α)
e : α → β
b : β
he₁ : UniformInducing e
he₂ : DenseInducing e
hs : s ∈ 𝓤 α
⊢ ∃ a, closure (e '' {a' | (a, a') ∈ s}) ∈ 𝓝 b
[PROOFSTEP]
obtain ⟨U, ⟨hU, hUo, hsymm⟩, hs⟩ : ∃ U, (U ∈ 𝓤 β ∧ IsOpen U ∧ SymmetricRel U) ∧ Prod.map e e ⁻¹' U ⊆ s := by
  rwa [← he₁.comap_uniformity, (uniformity_hasBasis_open_symmetric.comap _).mem_iff] at hs
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
s : Set (α × α)
e : α → β
b : β
he₁ : UniformInducing e
he₂ : DenseInducing e
hs : s ∈ 𝓤 α
⊢ ∃ U, (U ∈ 𝓤 β ∧ IsOpen U ∧ SymmetricRel U) ∧ Prod.map e e ⁻¹' U ⊆ s
[PROOFSTEP]
rwa [← he₁.comap_uniformity, (uniformity_hasBasis_open_symmetric.comap _).mem_iff] at hs
[GOAL]
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
s : Set (α × α)
e : α → β
b : β
he₁ : UniformInducing e
he₂ : DenseInducing e
hs✝ : s ∈ 𝓤 α
U : Set (β × β)
hs : Prod.map e e ⁻¹' U ⊆ s
hU : U ∈ 𝓤 β
hUo : IsOpen U
hsymm : SymmetricRel U
⊢ ∃ a, closure (e '' {a' | (a, a') ∈ s}) ∈ 𝓝 b
[PROOFSTEP]
rcases he₂.dense.mem_nhds (UniformSpace.ball_mem_nhds b hU) with ⟨a, ha⟩
[GOAL]
case intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
s : Set (α × α)
e : α → β
b : β
he₁ : UniformInducing e
he₂ : DenseInducing e
hs✝ : s ∈ 𝓤 α
U : Set (β × β)
hs : Prod.map e e ⁻¹' U ⊆ s
hU : U ∈ 𝓤 β
hUo : IsOpen U
hsymm : SymmetricRel U
a : α
ha : e a ∈ UniformSpace.ball b U
⊢ ∃ a, closure (e '' {a' | (a, a') ∈ s}) ∈ 𝓝 b
[PROOFSTEP]
refine ⟨a, mem_of_superset ?_ (closure_mono <| image_subset _ <| ball_mono hs a)⟩
[GOAL]
case intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
s : Set (α × α)
e : α → β
b : β
he₁ : UniformInducing e
he₂ : DenseInducing e
hs✝ : s ∈ 𝓤 α
U : Set (β × β)
hs : Prod.map e e ⁻¹' U ⊆ s
hU : U ∈ 𝓤 β
hUo : IsOpen U
hsymm : SymmetricRel U
a : α
ha : e a ∈ UniformSpace.ball b U
⊢ closure (e '' UniformSpace.ball a (Prod.map e e ⁻¹' U)) ∈ 𝓝 b
[PROOFSTEP]
have ho : IsOpen (UniformSpace.ball (e a) U) := UniformSpace.isOpen_ball (e a) hUo
[GOAL]
case intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
s : Set (α × α)
e : α → β
b : β
he₁ : UniformInducing e
he₂ : DenseInducing e
hs✝ : s ∈ 𝓤 α
U : Set (β × β)
hs : Prod.map e e ⁻¹' U ⊆ s
hU : U ∈ 𝓤 β
hUo : IsOpen U
hsymm : SymmetricRel U
a : α
ha : e a ∈ UniformSpace.ball b U
ho : IsOpen (UniformSpace.ball (e a) U)
⊢ closure (e '' UniformSpace.ball a (Prod.map e e ⁻¹' U)) ∈ 𝓝 b
[PROOFSTEP]
refine mem_of_superset (ho.mem_nhds <| (mem_ball_symmetry hsymm).2 ha) fun y hy => ?_
[GOAL]
case intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
s : Set (α × α)
e : α → β
b : β
he₁ : UniformInducing e
he₂ : DenseInducing e
hs✝ : s ∈ 𝓤 α
U : Set (β × β)
hs : Prod.map e e ⁻¹' U ⊆ s
hU : U ∈ 𝓤 β
hUo : IsOpen U
hsymm : SymmetricRel U
a : α
ha : e a ∈ UniformSpace.ball b U
ho : IsOpen (UniformSpace.ball (e a) U)
y : β
hy : y ∈ UniformSpace.ball (e a) U
⊢ y ∈ closure (e '' UniformSpace.ball a (Prod.map e e ⁻¹' U))
[PROOFSTEP]
refine mem_closure_iff_nhds.2 fun V hV => ?_
[GOAL]
case intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
s : Set (α × α)
e : α → β
b : β
he₁ : UniformInducing e
he₂ : DenseInducing e
hs✝ : s ∈ 𝓤 α
U : Set (β × β)
hs : Prod.map e e ⁻¹' U ⊆ s
hU : U ∈ 𝓤 β
hUo : IsOpen U
hsymm : SymmetricRel U
a : α
ha : e a ∈ UniformSpace.ball b U
ho : IsOpen (UniformSpace.ball (e a) U)
y : β
hy : y ∈ UniformSpace.ball (e a) U
V : Set β
hV : V ∈ 𝓝 y
⊢ Set.Nonempty (V ∩ e '' UniformSpace.ball a (Prod.map e e ⁻¹' U))
[PROOFSTEP]
rcases he₂.dense.mem_nhds (inter_mem hV (ho.mem_nhds hy)) with ⟨x, hxV, hxU⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
s : Set (α × α)
e : α → β
b : β
he₁ : UniformInducing e
he₂ : DenseInducing e
hs✝ : s ∈ 𝓤 α
U : Set (β × β)
hs : Prod.map e e ⁻¹' U ⊆ s
hU : U ∈ 𝓤 β
hUo : IsOpen U
hsymm : SymmetricRel U
a : α
ha : e a ∈ UniformSpace.ball b U
ho : IsOpen (UniformSpace.ball (e a) U)
y : β
hy : y ∈ UniformSpace.ball (e a) U
V : Set β
hV : V ∈ 𝓝 y
x : α
hxV : e x ∈ V
hxU : e x ∈ UniformSpace.ball (e a) U
⊢ Set.Nonempty (V ∩ e '' UniformSpace.ball a (Prod.map e e ⁻¹' U))
[PROOFSTEP]
exact ⟨e x, hxV, mem_image_of_mem e hxU⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
p : α → Prop
e : α → β
ue : UniformEmbedding e
de : DenseEmbedding e
⊢ comap (fun x => (DenseEmbedding.subtypeEmb p e x.fst, DenseEmbedding.subtypeEmb p e x.snd))
      (𝓤 { x // x ∈ closure (e '' {x | p x}) }) =
    𝓤 { x // p x }
[PROOFSTEP]
simp [comap_comap, (· ∘ ·), DenseEmbedding.subtypeEmb, uniformity_subtype, ue.comap_uniformity.symm]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
m : α → β
s : Set α
hm : UniformInducing m
hs : IsComplete (m '' s)
⊢ IsComplete s
[PROOFSTEP]
intro f hf hfs
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
m : α → β
s : Set α
hm : UniformInducing m
hs : IsComplete (m '' s)
f : Filter α
hf : Cauchy f
hfs : f ≤ 𝓟 s
⊢ ∃ x, x ∈ s ∧ f ≤ 𝓝 x
[PROOFSTEP]
rw [le_principal_iff] at hfs
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
m : α → β
s : Set α
hm : UniformInducing m
hs : IsComplete (m '' s)
f : Filter α
hf : Cauchy f
hfs : s ∈ f
⊢ ∃ x, x ∈ s ∧ f ≤ 𝓝 x
[PROOFSTEP]
obtain ⟨_, ⟨x, hx, rfl⟩, hyf⟩ : ∃ y ∈ m '' s, map m f ≤ 𝓝 y
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
m : α → β
s : Set α
hm : UniformInducing m
hs : IsComplete (m '' s)
f : Filter α
hf : Cauchy f
hfs : s ∈ f
⊢ ∃ y, y ∈ m '' s ∧ map m f ≤ 𝓝 y
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
m : α → β
s : Set α
hm : UniformInducing m
hs : IsComplete (m '' s)
f : Filter α
hf : Cauchy f
hfs : s ∈ f
x : α
hx : x ∈ s
hyf : map m f ≤ 𝓝 (m x)
⊢ ∃ x, x ∈ s ∧ f ≤ 𝓝 x
[PROOFSTEP]
exact hs (f.map m) (hf.map hm.uniformContinuous) (le_principal_iff.2 (image_mem_map hfs))
[GOAL]
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
m : α → β
s : Set α
hm : UniformInducing m
hs : IsComplete (m '' s)
f : Filter α
hf : Cauchy f
hfs : s ∈ f
x : α
hx : x ∈ s
hyf : map m f ≤ 𝓝 (m x)
⊢ ∃ x, x ∈ s ∧ f ≤ 𝓝 x
[PROOFSTEP]
rw [map_le_iff_le_comap, ← nhds_induced, ← hm.inducing.induced] at hyf
[GOAL]
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
m : α → β
s : Set α
hm : UniformInducing m
hs : IsComplete (m '' s)
f : Filter α
hf : Cauchy f
hfs : s ∈ f
x : α
hx : x ∈ s
hyf : f ≤ 𝓝 x
⊢ ∃ x, x ∈ s ∧ f ≤ 𝓝 x
[PROOFSTEP]
exact ⟨x, hx, hyf⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
s : Set α
hs : IsComplete s
⊢ IsComplete (Subtype.val '' univ)
[PROOFSTEP]
simp [hs]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
m : α → β
s : Set α
hm : UniformInducing m
⊢ IsComplete (m '' s) ↔ IsComplete s
[PROOFSTEP]
refine' ⟨isComplete_of_complete_image hm, fun c => _⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
m : α → β
s : Set α
hm : UniformInducing m
c : IsComplete s
⊢ IsComplete (m '' s)
[PROOFSTEP]
haveI : CompleteSpace s := c.completeSpace_coe
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
m : α → β
s : Set α
hm : UniformInducing m
c : IsComplete s
this : CompleteSpace ↑s
⊢ IsComplete (m '' s)
[PROOFSTEP]
set m' : s → β := m ∘ (↑)
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
m : α → β
s : Set α
hm : UniformInducing m
c : IsComplete s
this : CompleteSpace ↑s
m' : ↑s → β := m ∘ Subtype.val
⊢ IsComplete (m '' s)
[PROOFSTEP]
suffices IsComplete (range m') by rwa [range_comp, Subtype.range_coe] at this
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
m : α → β
s : Set α
hm : UniformInducing m
c : IsComplete s
this✝ : CompleteSpace ↑s
m' : ↑s → β := m ∘ Subtype.val
this : IsComplete (range m')
⊢ IsComplete (m '' s)
[PROOFSTEP]
rwa [range_comp, Subtype.range_coe] at this
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
m : α → β
s : Set α
hm : UniformInducing m
c : IsComplete s
this : CompleteSpace ↑s
m' : ↑s → β := m ∘ Subtype.val
⊢ IsComplete (range m')
[PROOFSTEP]
have hm' : UniformInducing m' := hm.comp uniformEmbedding_subtype_val.toUniformInducing
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
m : α → β
s : Set α
hm : UniformInducing m
c : IsComplete s
this : CompleteSpace ↑s
m' : ↑s → β := m ∘ Subtype.val
hm' : UniformInducing m'
⊢ IsComplete (range m')
[PROOFSTEP]
intro f hf hfm
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
m : α → β
s : Set α
hm : UniformInducing m
c : IsComplete s
this : CompleteSpace ↑s
m' : ↑s → β := m ∘ Subtype.val
hm' : UniformInducing m'
f : Filter β
hf : Cauchy f
hfm : f ≤ 𝓟 (range m')
⊢ ∃ x, x ∈ range m' ∧ f ≤ 𝓝 x
[PROOFSTEP]
rw [Filter.le_principal_iff] at hfm
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
m : α → β
s : Set α
hm : UniformInducing m
c : IsComplete s
this : CompleteSpace ↑s
m' : ↑s → β := m ∘ Subtype.val
hm' : UniformInducing m'
f : Filter β
hf : Cauchy f
hfm : range m' ∈ f
⊢ ∃ x, x ∈ range m' ∧ f ≤ 𝓝 x
[PROOFSTEP]
have cf' : Cauchy (comap m' f) := hf.comap' hm'.comap_uniformity.le (NeBot.comap_of_range_mem hf.1 hfm)
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
m : α → β
s : Set α
hm : UniformInducing m
c : IsComplete s
this : CompleteSpace ↑s
m' : ↑s → β := m ∘ Subtype.val
hm' : UniformInducing m'
f : Filter β
hf : Cauchy f
hfm : range m' ∈ f
cf' : Cauchy (comap m' f)
⊢ ∃ x, x ∈ range m' ∧ f ≤ 𝓝 x
[PROOFSTEP]
rcases CompleteSpace.complete cf' with ⟨x, hx⟩
[GOAL]
case intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
m : α → β
s : Set α
hm : UniformInducing m
c : IsComplete s
this : CompleteSpace ↑s
m' : ↑s → β := m ∘ Subtype.val
hm' : UniformInducing m'
f : Filter β
hf : Cauchy f
hfm : range m' ∈ f
cf' : Cauchy (comap m' f)
x : ↑s
hx : comap m' f ≤ 𝓝 x
⊢ ∃ x, x ∈ range m' ∧ f ≤ 𝓝 x
[PROOFSTEP]
rw [hm'.inducing.nhds_eq_comap, comap_le_comap_iff hfm] at hx
[GOAL]
case intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
m : α → β
s : Set α
hm : UniformInducing m
c : IsComplete s
this : CompleteSpace ↑s
m' : ↑s → β := m ∘ Subtype.val
hm' : UniformInducing m'
f : Filter β
hf : Cauchy f
hfm : range m' ∈ f
cf' : Cauchy (comap m' f)
x : ↑s
hx : f ≤ 𝓝 (m' x)
⊢ ∃ x, x ∈ range m' ∧ f ≤ 𝓝 x
[PROOFSTEP]
exact ⟨m' x, mem_range_self _, hx⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
hf : UniformInducing f
⊢ CompleteSpace α ↔ IsComplete (range f)
[PROOFSTEP]
rw [completeSpace_iff_isComplete_univ, ← isComplete_image_iff hf, image_univ]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
e : α ≃ β
he : UniformEmbedding ↑e
⊢ CompleteSpace α ↔ CompleteSpace β
[PROOFSTEP]
rw [completeSpace_iff_isComplete_range he.toUniformInducing, e.range_eq_univ, completeSpace_iff_isComplete_univ]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
s : Set α
⊢ IsComplete (range Subtype.val) ↔ IsComplete s
[PROOFSTEP]
rw [Subtype.range_coe]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
m : β → α
hm : UniformInducing m
dense : DenseRange m
h : ∀ (f : Filter β), Cauchy f → ∃ x, map m f ≤ 𝓝 x
f : Filter α
hf : Cauchy f
p : Set (α × α) → Set α → Set α := fun s t => {y | ∃ x, x ∈ t ∧ (x, y) ∈ s}
g : Filter α := Filter.lift (𝓤 α) fun s => Filter.lift' f (p s)
mp₀ : Monotone p
mp₁ : ∀ {s : Set (α × α)}, Monotone (p s)
this✝⁵ : f ≤ g
this✝⁴ : NeBot g
this✝³ : NeBot (comap m g)
this✝² : Cauchy g
this✝¹ : Cauchy (comap m g)
x : α
hx : map m (comap m g) ≤ 𝓝 x
this✝ : ClusterPt x (map m (comap m g))
this : ClusterPt x g
⊢ f ≤ g
[PROOFSTEP]
assumption
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
s : Set β
hf : UniformEmbedding f
hs : TotallyBounded s
t : Set (α × α)
ht : t ∈ 𝓤 α
⊢ ∃ t_1, Set.Finite t_1 ∧ f ⁻¹' s ⊆ ⋃ (y : α) (_ : y ∈ t_1), {x | (x, y) ∈ t}
[PROOFSTEP]
rw [← hf.comap_uniformity] at ht
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
s : Set β
hf : UniformEmbedding f
hs : TotallyBounded s
t : Set (α × α)
ht : t ∈ comap (fun x => (f x.fst, f x.snd)) (𝓤 β)
⊢ ∃ t_1, Set.Finite t_1 ∧ f ⁻¹' s ⊆ ⋃ (y : α) (_ : y ∈ t_1), {x | (x, y) ∈ t}
[PROOFSTEP]
rcases mem_comap.2 ht with ⟨t', ht', ts⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
s : Set β
hf : UniformEmbedding f
hs : TotallyBounded s
t : Set (α × α)
ht : t ∈ comap (fun x => (f x.fst, f x.snd)) (𝓤 β)
t' : Set (β × β)
ht' : t' ∈ 𝓤 β
ts : (fun x => (f x.fst, f x.snd)) ⁻¹' t' ⊆ t
⊢ ∃ t_1, Set.Finite t_1 ∧ f ⁻¹' s ⊆ ⋃ (y : α) (_ : y ∈ t_1), {x | (x, y) ∈ t}
[PROOFSTEP]
rcases totallyBounded_iff_subset.1 (totallyBounded_subset (image_preimage_subset f s) hs) _ ht' with ⟨c, cs, hfc, hct⟩
[GOAL]
case intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
s : Set β
hf : UniformEmbedding f
hs : TotallyBounded s
t : Set (α × α)
ht : t ∈ comap (fun x => (f x.fst, f x.snd)) (𝓤 β)
t' : Set (β × β)
ht' : t' ∈ 𝓤 β
ts : (fun x => (f x.fst, f x.snd)) ⁻¹' t' ⊆ t
c : Set β
cs : c ⊆ f '' (f ⁻¹' s)
hfc : Set.Finite c
hct : f '' (f ⁻¹' s) ⊆ ⋃ (y : β) (_ : y ∈ c), {x | (x, y) ∈ t'}
⊢ ∃ t_1, Set.Finite t_1 ∧ f ⁻¹' s ⊆ ⋃ (y : α) (_ : y ∈ t_1), {x | (x, y) ∈ t}
[PROOFSTEP]
refine' ⟨f ⁻¹' c, hfc.preimage (hf.inj.injOn _), fun x h => _⟩
[GOAL]
case intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
s : Set β
hf : UniformEmbedding f
hs : TotallyBounded s
t : Set (α × α)
ht : t ∈ comap (fun x => (f x.fst, f x.snd)) (𝓤 β)
t' : Set (β × β)
ht' : t' ∈ 𝓤 β
ts : (fun x => (f x.fst, f x.snd)) ⁻¹' t' ⊆ t
c : Set β
cs : c ⊆ f '' (f ⁻¹' s)
hfc : Set.Finite c
hct : f '' (f ⁻¹' s) ⊆ ⋃ (y : β) (_ : y ∈ c), {x | (x, y) ∈ t'}
x : α
h : x ∈ f ⁻¹' s
⊢ x ∈ ⋃ (y : α) (_ : y ∈ f ⁻¹' c), {x | (x, y) ∈ t}
[PROOFSTEP]
have := hct (mem_image_of_mem f h)
[GOAL]
case intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
s : Set β
hf : UniformEmbedding f
hs : TotallyBounded s
t : Set (α × α)
ht : t ∈ comap (fun x => (f x.fst, f x.snd)) (𝓤 β)
t' : Set (β × β)
ht' : t' ∈ 𝓤 β
ts : (fun x => (f x.fst, f x.snd)) ⁻¹' t' ⊆ t
c : Set β
cs : c ⊆ f '' (f ⁻¹' s)
hfc : Set.Finite c
hct : f '' (f ⁻¹' s) ⊆ ⋃ (y : β) (_ : y ∈ c), {x | (x, y) ∈ t'}
x : α
h : x ∈ f ⁻¹' s
this : f x ∈ ⋃ (y : β) (_ : y ∈ c), {x | (x, y) ∈ t'}
⊢ x ∈ ⋃ (y : α) (_ : y ∈ f ⁻¹' c), {x | (x, y) ∈ t}
[PROOFSTEP]
simp at this ⊢
[GOAL]
case intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
s : Set β
hf : UniformEmbedding f
hs : TotallyBounded s
t : Set (α × α)
ht : t ∈ comap (fun x => (f x.fst, f x.snd)) (𝓤 β)
t' : Set (β × β)
ht' : t' ∈ 𝓤 β
ts : (fun x => (f x.fst, f x.snd)) ⁻¹' t' ⊆ t
c : Set β
cs : c ⊆ f '' (f ⁻¹' s)
hfc : Set.Finite c
hct : f '' (f ⁻¹' s) ⊆ ⋃ (y : β) (_ : y ∈ c), {x | (x, y) ∈ t'}
x : α
h : x ∈ f ⁻¹' s
this : ∃ i, i ∈ c ∧ (f x, i) ∈ t'
⊢ ∃ i, f i ∈ c ∧ (x, i) ∈ t
[PROOFSTEP]
rcases this with ⟨z, zc, zt⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
s : Set β
hf : UniformEmbedding f
hs : TotallyBounded s
t : Set (α × α)
ht : t ∈ comap (fun x => (f x.fst, f x.snd)) (𝓤 β)
t' : Set (β × β)
ht' : t' ∈ 𝓤 β
ts : (fun x => (f x.fst, f x.snd)) ⁻¹' t' ⊆ t
c : Set β
cs : c ⊆ f '' (f ⁻¹' s)
hfc : Set.Finite c
hct : f '' (f ⁻¹' s) ⊆ ⋃ (y : β) (_ : y ∈ c), {x | (x, y) ∈ t'}
x : α
h : x ∈ f ⁻¹' s
z : β
zc : z ∈ c
zt : (f x, z) ∈ t'
⊢ ∃ i, f i ∈ c ∧ (x, i) ∈ t
[PROOFSTEP]
rcases cs zc with ⟨y, -, rfl⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
s : Set β
hf : UniformEmbedding f
hs : TotallyBounded s
t : Set (α × α)
ht : t ∈ comap (fun x => (f x.fst, f x.snd)) (𝓤 β)
t' : Set (β × β)
ht' : t' ∈ 𝓤 β
ts : (fun x => (f x.fst, f x.snd)) ⁻¹' t' ⊆ t
c : Set β
cs : c ⊆ f '' (f ⁻¹' s)
hfc : Set.Finite c
hct : f '' (f ⁻¹' s) ⊆ ⋃ (y : β) (_ : y ∈ c), {x | (x, y) ∈ t'}
x : α
h : x ∈ f ⁻¹' s
y : α
zc : f y ∈ c
zt : (f x, f y) ∈ t'
⊢ ∃ i, f i ∈ c ∧ (x, i) ∈ t
[PROOFSTEP]
exact ⟨y, zc, ts zt⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : UniformSpace γ
inst✝¹ : CompleteSpace α
inst✝ : CompleteSpace β
⊢ CompleteSpace (α ⊕ β)
[PROOFSTEP]
rw [completeSpace_iff_isComplete_univ, ← range_inl_union_range_inr]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : UniformSpace γ
inst✝¹ : CompleteSpace α
inst✝ : CompleteSpace β
⊢ IsComplete (range Sum.inl ∪ range Sum.inr)
[PROOFSTEP]
exact
  uniformEmbedding_inl.toUniformInducing.isComplete_range.union uniformEmbedding_inr.toUniformInducing.isComplete_range
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
e✝ : β → α
h_e : UniformInducing e✝
h_dense : DenseRange e✝
f✝ : β → γ
h_f : UniformContinuous f✝
inst✝ : CompleteSpace γ
p : α → Prop
e : α → β
f : α → γ
b : β
s : Set α
hf : UniformContinuous fun x => f ↑x
he : UniformEmbedding e
hd : ∀ (x : β), x ∈ closure (range e)
hb : closure (e '' s) ∈ 𝓝 b
hs : IsClosed s
hp : ∀ (x : α), x ∈ s → p x
⊢ ∃ c, Tendsto f (comap e (𝓝 b)) (𝓝 c)
[PROOFSTEP]
have de : DenseEmbedding e := he.denseEmbedding hd
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
e✝ : β → α
h_e : UniformInducing e✝
h_dense : DenseRange e✝
f✝ : β → γ
h_f : UniformContinuous f✝
inst✝ : CompleteSpace γ
p : α → Prop
e : α → β
f : α → γ
b : β
s : Set α
hf : UniformContinuous fun x => f ↑x
he : UniformEmbedding e
hd : ∀ (x : β), x ∈ closure (range e)
hb : closure (e '' s) ∈ 𝓝 b
hs : IsClosed s
hp : ∀ (x : α), x ∈ s → p x
de : DenseEmbedding e
⊢ ∃ c, Tendsto f (comap e (𝓝 b)) (𝓝 c)
[PROOFSTEP]
have de' : DenseEmbedding (DenseEmbedding.subtypeEmb p e) := de.subtype p
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
e✝ : β → α
h_e : UniformInducing e✝
h_dense : DenseRange e✝
f✝ : β → γ
h_f : UniformContinuous f✝
inst✝ : CompleteSpace γ
p : α → Prop
e : α → β
f : α → γ
b : β
s : Set α
hf : UniformContinuous fun x => f ↑x
he : UniformEmbedding e
hd : ∀ (x : β), x ∈ closure (range e)
hb : closure (e '' s) ∈ 𝓝 b
hs : IsClosed s
hp : ∀ (x : α), x ∈ s → p x
de : DenseEmbedding e
de' : DenseEmbedding (DenseEmbedding.subtypeEmb p e)
⊢ ∃ c, Tendsto f (comap e (𝓝 b)) (𝓝 c)
[PROOFSTEP]
have ue' : UniformEmbedding (DenseEmbedding.subtypeEmb p e) := uniformEmbedding_subtypeEmb _ he de
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
e✝ : β → α
h_e : UniformInducing e✝
h_dense : DenseRange e✝
f✝ : β → γ
h_f : UniformContinuous f✝
inst✝ : CompleteSpace γ
p : α → Prop
e : α → β
f : α → γ
b : β
s : Set α
hf : UniformContinuous fun x => f ↑x
he : UniformEmbedding e
hd : ∀ (x : β), x ∈ closure (range e)
hb : closure (e '' s) ∈ 𝓝 b
hs : IsClosed s
hp : ∀ (x : α), x ∈ s → p x
de : DenseEmbedding e
de' : DenseEmbedding (DenseEmbedding.subtypeEmb p e)
ue' : UniformEmbedding (DenseEmbedding.subtypeEmb p e)
⊢ ∃ c, Tendsto f (comap e (𝓝 b)) (𝓝 c)
[PROOFSTEP]
have : b ∈ closure (e '' {x | p x}) := (closure_mono <| monotone_image <| hp) (mem_of_mem_nhds hb)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
e✝ : β → α
h_e : UniformInducing e✝
h_dense : DenseRange e✝
f✝ : β → γ
h_f : UniformContinuous f✝
inst✝ : CompleteSpace γ
p : α → Prop
e : α → β
f : α → γ
b : β
s : Set α
hf : UniformContinuous fun x => f ↑x
he : UniformEmbedding e
hd : ∀ (x : β), x ∈ closure (range e)
hb : closure (e '' s) ∈ 𝓝 b
hs : IsClosed s
hp : ∀ (x : α), x ∈ s → p x
de : DenseEmbedding e
de' : DenseEmbedding (DenseEmbedding.subtypeEmb p e)
ue' : UniformEmbedding (DenseEmbedding.subtypeEmb p e)
this : b ∈ closure (e '' {x | p x})
⊢ ∃ c, Tendsto f (comap e (𝓝 b)) (𝓝 c)
[PROOFSTEP]
let ⟨c, hc⟩ := uniformly_extend_exists ue'.toUniformInducing de'.dense hf ⟨b, this⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
e✝ : β → α
h_e : UniformInducing e✝
h_dense : DenseRange e✝
f✝ : β → γ
h_f : UniformContinuous f✝
inst✝ : CompleteSpace γ
p : α → Prop
e : α → β
f : α → γ
b : β
s : Set α
hf : UniformContinuous fun x => f ↑x
he : UniformEmbedding e
hd : ∀ (x : β), x ∈ closure (range e)
hb : closure (e '' s) ∈ 𝓝 b
hs : IsClosed s
hp : ∀ (x : α), x ∈ s → p x
de : DenseEmbedding e
de' : DenseEmbedding (DenseEmbedding.subtypeEmb p e)
ue' : UniformEmbedding (DenseEmbedding.subtypeEmb p e)
this : b ∈ closure (e '' {x | p x})
c : γ
hc : Tendsto (fun x => f ↑x) (comap (DenseEmbedding.subtypeEmb p e) (𝓝 { val := b, property := this })) (𝓝 c)
⊢ ∃ c, Tendsto f (comap e (𝓝 b)) (𝓝 c)
[PROOFSTEP]
replace hc : Tendsto (f ∘ Subtype.val) (((𝓝 b).comap e).comap Subtype.val) (𝓝 c) := by
  simpa only [nhds_subtype_eq_comap, comap_comap, DenseEmbedding.subtypeEmb_coe] using hc
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
e✝ : β → α
h_e : UniformInducing e✝
h_dense : DenseRange e✝
f✝ : β → γ
h_f : UniformContinuous f✝
inst✝ : CompleteSpace γ
p : α → Prop
e : α → β
f : α → γ
b : β
s : Set α
hf : UniformContinuous fun x => f ↑x
he : UniformEmbedding e
hd : ∀ (x : β), x ∈ closure (range e)
hb : closure (e '' s) ∈ 𝓝 b
hs : IsClosed s
hp : ∀ (x : α), x ∈ s → p x
de : DenseEmbedding e
de' : DenseEmbedding (DenseEmbedding.subtypeEmb p e)
ue' : UniformEmbedding (DenseEmbedding.subtypeEmb p e)
this : b ∈ closure (e '' {x | p x})
c : γ
hc : Tendsto (fun x => f ↑x) (comap (DenseEmbedding.subtypeEmb p e) (𝓝 { val := b, property := this })) (𝓝 c)
⊢ Tendsto (f ∘ Subtype.val) (comap Subtype.val (comap e (𝓝 b))) (𝓝 c)
[PROOFSTEP]
simpa only [nhds_subtype_eq_comap, comap_comap, DenseEmbedding.subtypeEmb_coe] using hc
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
e✝ : β → α
h_e : UniformInducing e✝
h_dense : DenseRange e✝
f✝ : β → γ
h_f : UniformContinuous f✝
inst✝ : CompleteSpace γ
p : α → Prop
e : α → β
f : α → γ
b : β
s : Set α
hf : UniformContinuous fun x => f ↑x
he : UniformEmbedding e
hd : ∀ (x : β), x ∈ closure (range e)
hb : closure (e '' s) ∈ 𝓝 b
hs : IsClosed s
hp : ∀ (x : α), x ∈ s → p x
de : DenseEmbedding e
de' : DenseEmbedding (DenseEmbedding.subtypeEmb p e)
ue' : UniformEmbedding (DenseEmbedding.subtypeEmb p e)
this : b ∈ closure (e '' {x | p x})
c : γ
hc : Tendsto (f ∘ Subtype.val) (comap Subtype.val (comap e (𝓝 b))) (𝓝 c)
⊢ ∃ c, Tendsto f (comap e (𝓝 b)) (𝓝 c)
[PROOFSTEP]
refine ⟨c, (tendsto_comap'_iff ?_).1 hc⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
e✝ : β → α
h_e : UniformInducing e✝
h_dense : DenseRange e✝
f✝ : β → γ
h_f : UniformContinuous f✝
inst✝ : CompleteSpace γ
p : α → Prop
e : α → β
f : α → γ
b : β
s : Set α
hf : UniformContinuous fun x => f ↑x
he : UniformEmbedding e
hd : ∀ (x : β), x ∈ closure (range e)
hb : closure (e '' s) ∈ 𝓝 b
hs : IsClosed s
hp : ∀ (x : α), x ∈ s → p x
de : DenseEmbedding e
de' : DenseEmbedding (DenseEmbedding.subtypeEmb p e)
ue' : UniformEmbedding (DenseEmbedding.subtypeEmb p e)
this : b ∈ closure (e '' {x | p x})
c : γ
hc : Tendsto (f ∘ Subtype.val) (comap Subtype.val (comap e (𝓝 b))) (𝓝 c)
⊢ range Subtype.val ∈ comap e (𝓝 b)
[PROOFSTEP]
rw [Subtype.range_coe_subtype]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
e✝ : β → α
h_e : UniformInducing e✝
h_dense : DenseRange e✝
f✝ : β → γ
h_f : UniformContinuous f✝
inst✝ : CompleteSpace γ
p : α → Prop
e : α → β
f : α → γ
b : β
s : Set α
hf : UniformContinuous fun x => f ↑x
he : UniformEmbedding e
hd : ∀ (x : β), x ∈ closure (range e)
hb : closure (e '' s) ∈ 𝓝 b
hs : IsClosed s
hp : ∀ (x : α), x ∈ s → p x
de : DenseEmbedding e
de' : DenseEmbedding (DenseEmbedding.subtypeEmb p e)
ue' : UniformEmbedding (DenseEmbedding.subtypeEmb p e)
this : b ∈ closure (e '' {x | p x})
c : γ
hc : Tendsto (f ∘ Subtype.val) (comap Subtype.val (comap e (𝓝 b))) (𝓝 c)
⊢ {x | p x} ∈ comap e (𝓝 b)
[PROOFSTEP]
exact ⟨_, hb, by rwa [← de.toInducing.closure_eq_preimage_closure_image, hs.closure_eq]⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
e✝ : β → α
h_e : UniformInducing e✝
h_dense : DenseRange e✝
f✝ : β → γ
h_f : UniformContinuous f✝
inst✝ : CompleteSpace γ
p : α → Prop
e : α → β
f : α → γ
b : β
s : Set α
hf : UniformContinuous fun x => f ↑x
he : UniformEmbedding e
hd : ∀ (x : β), x ∈ closure (range e)
hb : closure (e '' s) ∈ 𝓝 b
hs : IsClosed s
hp : ∀ (x : α), x ∈ s → p x
de : DenseEmbedding e
de' : DenseEmbedding (DenseEmbedding.subtypeEmb p e)
ue' : UniformEmbedding (DenseEmbedding.subtypeEmb p e)
this : b ∈ closure (e '' {x | p x})
c : γ
hc : Tendsto (f ∘ Subtype.val) (comap Subtype.val (comap e (𝓝 b))) (𝓝 c)
⊢ e ⁻¹' closure (e '' s) ⊆ {x | p x}
[PROOFSTEP]
rwa [← de.toInducing.closure_eq_preimage_closure_image, hs.closure_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
e : β → α
h_e : UniformInducing e
h_dense : DenseRange e
f : β → γ
h_f : UniformContinuous f
inst✝ : CompleteSpace γ
a : α
⊢ Tendsto f (comap e (𝓝 a)) (𝓝 (DenseInducing.extend (_ : DenseInducing e) f a))
[PROOFSTEP]
simpa only [DenseInducing.extend] using tendsto_nhds_limUnder (uniformly_extend_exists h_e ‹_› h_f _)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
e : β → α
h_e : UniformInducing e
h_dense : DenseRange e
f : β → γ
h_f : UniformContinuous f
inst✝ : CompleteSpace γ
d : Set (γ × γ)
hd : d ∈ 𝓤 γ
s : Set (γ × γ)
hs : s ∈ 𝓤 γ
hs_comp : s ○ (s ○ s) ⊆ d
h_pnt :
  ∀ {a : α} {m : Set α},
    m ∈ 𝓝 a →
      ∃ c,
        c ∈ f '' (e ⁻¹' m) ∧
          (c, DenseInducing.extend (_ : DenseInducing e) f a) ∈ s ∧
            (DenseInducing.extend (_ : DenseInducing e) f a, c) ∈ s
this : Prod.map f f ⁻¹' s ∈ 𝓤 β
⊢ Prod.map f f ⁻¹' s ∈ comap (Prod.map e e) (𝓤 α)
[PROOFSTEP]
rwa [← h_e.comap_uniformity] at this
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
e : β → α
h_e : UniformInducing e
h_dense : DenseRange e
f : β → γ
h_f : UniformContinuous f
inst✝ : CompleteSpace γ
d : Set (γ × γ)
hd : d ∈ 𝓤 γ
s : Set (γ × γ)
hs : s ∈ 𝓤 γ
hs_comp : s ○ (s ○ s) ⊆ d
h_pnt :
  ∀ {a : α} {m : Set α},
    m ∈ 𝓝 a →
      ∃ c,
        c ∈ f '' (e ⁻¹' m) ∧
          (c, DenseInducing.extend (_ : DenseInducing e) f a) ∈ s ∧
            (DenseInducing.extend (_ : DenseInducing e) f a, c) ∈ s
this✝ : Prod.map f f ⁻¹' s ∈ 𝓤 β
this : Prod.map f f ⁻¹' s ∈ comap (Prod.map e e) (𝓤 α)
t : Set (α × α)
ht : t ∈ 𝓤 α
ts : Prod.map e e ⁻¹' t ⊆ Prod.map f f ⁻¹' s
x✝ : α × α
x₁ x₂ : α
hx_t : (x₁, x₂) ∈ interior t
⊢ (x₁, x₂) ∈
    Prod.map (DenseInducing.extend (_ : DenseInducing e) f) (DenseInducing.extend (_ : DenseInducing e) f) ⁻¹' d
[PROOFSTEP]
have : interior t ∈ 𝓝 (x₁, x₂) := isOpen_interior.mem_nhds hx_t
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
e : β → α
h_e : UniformInducing e
h_dense : DenseRange e
f : β → γ
h_f : UniformContinuous f
inst✝ : CompleteSpace γ
d : Set (γ × γ)
hd : d ∈ 𝓤 γ
s : Set (γ × γ)
hs : s ∈ 𝓤 γ
hs_comp : s ○ (s ○ s) ⊆ d
h_pnt :
  ∀ {a : α} {m : Set α},
    m ∈ 𝓝 a →
      ∃ c,
        c ∈ f '' (e ⁻¹' m) ∧
          (c, DenseInducing.extend (_ : DenseInducing e) f a) ∈ s ∧
            (DenseInducing.extend (_ : DenseInducing e) f a, c) ∈ s
this✝¹ : Prod.map f f ⁻¹' s ∈ 𝓤 β
this✝ : Prod.map f f ⁻¹' s ∈ comap (Prod.map e e) (𝓤 α)
t : Set (α × α)
ht : t ∈ 𝓤 α
ts : Prod.map e e ⁻¹' t ⊆ Prod.map f f ⁻¹' s
x✝ : α × α
x₁ x₂ : α
hx_t : (x₁, x₂) ∈ interior t
this : interior t ∈ 𝓝 (x₁, x₂)
⊢ (x₁, x₂) ∈
    Prod.map (DenseInducing.extend (_ : DenseInducing e) f) (DenseInducing.extend (_ : DenseInducing e) f) ⁻¹' d
[PROOFSTEP]
let ⟨m₁, hm₁, m₂, hm₂, (hm : m₁ ×ˢ m₂ ⊆ interior t)⟩ := mem_nhds_prod_iff.mp this
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
e : β → α
h_e : UniformInducing e
h_dense : DenseRange e
f : β → γ
h_f : UniformContinuous f
inst✝ : CompleteSpace γ
d : Set (γ × γ)
hd : d ∈ 𝓤 γ
s : Set (γ × γ)
hs : s ∈ 𝓤 γ
hs_comp : s ○ (s ○ s) ⊆ d
h_pnt :
  ∀ {a : α} {m : Set α},
    m ∈ 𝓝 a →
      ∃ c,
        c ∈ f '' (e ⁻¹' m) ∧
          (c, DenseInducing.extend (_ : DenseInducing e) f a) ∈ s ∧
            (DenseInducing.extend (_ : DenseInducing e) f a, c) ∈ s
this✝¹ : Prod.map f f ⁻¹' s ∈ 𝓤 β
this✝ : Prod.map f f ⁻¹' s ∈ comap (Prod.map e e) (𝓤 α)
t : Set (α × α)
ht : t ∈ 𝓤 α
ts : Prod.map e e ⁻¹' t ⊆ Prod.map f f ⁻¹' s
x✝ : α × α
x₁ x₂ : α
hx_t : (x₁, x₂) ∈ interior t
this : interior t ∈ 𝓝 (x₁, x₂)
m₁ : Set α
hm₁ : m₁ ∈ 𝓝 x₁
m₂ : Set α
hm₂ : m₂ ∈ 𝓝 x₂
hm : m₁ ×ˢ m₂ ⊆ interior t
⊢ (x₁, x₂) ∈
    Prod.map (DenseInducing.extend (_ : DenseInducing e) f) (DenseInducing.extend (_ : DenseInducing e) f) ⁻¹' d
[PROOFSTEP]
obtain ⟨_, ⟨a, ha₁, rfl⟩, _, ha₂⟩ := h_pnt hm₁
[GOAL]
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
e : β → α
h_e : UniformInducing e
h_dense : DenseRange e
f : β → γ
h_f : UniformContinuous f
inst✝ : CompleteSpace γ
d : Set (γ × γ)
hd : d ∈ 𝓤 γ
s : Set (γ × γ)
hs : s ∈ 𝓤 γ
hs_comp : s ○ (s ○ s) ⊆ d
h_pnt :
  ∀ {a : α} {m : Set α},
    m ∈ 𝓝 a →
      ∃ c,
        c ∈ f '' (e ⁻¹' m) ∧
          (c, DenseInducing.extend (_ : DenseInducing e) f a) ∈ s ∧
            (DenseInducing.extend (_ : DenseInducing e) f a, c) ∈ s
this✝¹ : Prod.map f f ⁻¹' s ∈ 𝓤 β
this✝ : Prod.map f f ⁻¹' s ∈ comap (Prod.map e e) (𝓤 α)
t : Set (α × α)
ht : t ∈ 𝓤 α
ts : Prod.map e e ⁻¹' t ⊆ Prod.map f f ⁻¹' s
x✝ : α × α
x₁ x₂ : α
hx_t : (x₁, x₂) ∈ interior t
this : interior t ∈ 𝓝 (x₁, x₂)
m₁ : Set α
hm₁ : m₁ ∈ 𝓝 x₁
m₂ : Set α
hm₂ : m₂ ∈ 𝓝 x₂
hm : m₁ ×ˢ m₂ ⊆ interior t
a : β
ha₁ : a ∈ e ⁻¹' m₁
left✝ : (f a, DenseInducing.extend (_ : DenseInducing e) f x₁) ∈ s
ha₂ : (DenseInducing.extend (_ : DenseInducing e) f x₁, f a) ∈ s
⊢ (x₁, x₂) ∈
    Prod.map (DenseInducing.extend (_ : DenseInducing e) f) (DenseInducing.extend (_ : DenseInducing e) f) ⁻¹' d
[PROOFSTEP]
obtain ⟨_, ⟨b, hb₁, rfl⟩, hb₂, _⟩ := h_pnt hm₂
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
e : β → α
h_e : UniformInducing e
h_dense : DenseRange e
f : β → γ
h_f : UniformContinuous f
inst✝ : CompleteSpace γ
d : Set (γ × γ)
hd : d ∈ 𝓤 γ
s : Set (γ × γ)
hs : s ∈ 𝓤 γ
hs_comp : s ○ (s ○ s) ⊆ d
h_pnt :
  ∀ {a : α} {m : Set α},
    m ∈ 𝓝 a →
      ∃ c,
        c ∈ f '' (e ⁻¹' m) ∧
          (c, DenseInducing.extend (_ : DenseInducing e) f a) ∈ s ∧
            (DenseInducing.extend (_ : DenseInducing e) f a, c) ∈ s
this✝¹ : Prod.map f f ⁻¹' s ∈ 𝓤 β
this✝ : Prod.map f f ⁻¹' s ∈ comap (Prod.map e e) (𝓤 α)
t : Set (α × α)
ht : t ∈ 𝓤 α
ts : Prod.map e e ⁻¹' t ⊆ Prod.map f f ⁻¹' s
x✝ : α × α
x₁ x₂ : α
hx_t : (x₁, x₂) ∈ interior t
this : interior t ∈ 𝓝 (x₁, x₂)
m₁ : Set α
hm₁ : m₁ ∈ 𝓝 x₁
m₂ : Set α
hm₂ : m₂ ∈ 𝓝 x₂
hm : m₁ ×ˢ m₂ ⊆ interior t
a : β
ha₁ : a ∈ e ⁻¹' m₁
left✝ : (f a, DenseInducing.extend (_ : DenseInducing e) f x₁) ∈ s
ha₂ : (DenseInducing.extend (_ : DenseInducing e) f x₁, f a) ∈ s
b : β
hb₁ : b ∈ e ⁻¹' m₂
hb₂ : (f b, DenseInducing.extend (_ : DenseInducing e) f x₂) ∈ s
right✝ : (DenseInducing.extend (_ : DenseInducing e) f x₂, f b) ∈ s
⊢ (x₁, x₂) ∈
    Prod.map (DenseInducing.extend (_ : DenseInducing e) f) (DenseInducing.extend (_ : DenseInducing e) f) ⁻¹' d
[PROOFSTEP]
have : Prod.map f f (a, b) ∈ s := ts <| mem_preimage.2 <| interior_subset (@hm (e a, e b) ⟨ha₁, hb₁⟩)
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
e : β → α
h_e : UniformInducing e
h_dense : DenseRange e
f : β → γ
h_f : UniformContinuous f
inst✝ : CompleteSpace γ
d : Set (γ × γ)
hd : d ∈ 𝓤 γ
s : Set (γ × γ)
hs : s ∈ 𝓤 γ
hs_comp : s ○ (s ○ s) ⊆ d
h_pnt :
  ∀ {a : α} {m : Set α},
    m ∈ 𝓝 a →
      ∃ c,
        c ∈ f '' (e ⁻¹' m) ∧
          (c, DenseInducing.extend (_ : DenseInducing e) f a) ∈ s ∧
            (DenseInducing.extend (_ : DenseInducing e) f a, c) ∈ s
this✝² : Prod.map f f ⁻¹' s ∈ 𝓤 β
this✝¹ : Prod.map f f ⁻¹' s ∈ comap (Prod.map e e) (𝓤 α)
t : Set (α × α)
ht : t ∈ 𝓤 α
ts : Prod.map e e ⁻¹' t ⊆ Prod.map f f ⁻¹' s
x✝ : α × α
x₁ x₂ : α
hx_t : (x₁, x₂) ∈ interior t
this✝ : interior t ∈ 𝓝 (x₁, x₂)
m₁ : Set α
hm₁ : m₁ ∈ 𝓝 x₁
m₂ : Set α
hm₂ : m₂ ∈ 𝓝 x₂
hm : m₁ ×ˢ m₂ ⊆ interior t
a : β
ha₁ : a ∈ e ⁻¹' m₁
left✝ : (f a, DenseInducing.extend (_ : DenseInducing e) f x₁) ∈ s
ha₂ : (DenseInducing.extend (_ : DenseInducing e) f x₁, f a) ∈ s
b : β
hb₁ : b ∈ e ⁻¹' m₂
hb₂ : (f b, DenseInducing.extend (_ : DenseInducing e) f x₂) ∈ s
right✝ : (DenseInducing.extend (_ : DenseInducing e) f x₂, f b) ∈ s
this : Prod.map f f (a, b) ∈ s
⊢ (x₁, x₂) ∈
    Prod.map (DenseInducing.extend (_ : DenseInducing e) f) (DenseInducing.extend (_ : DenseInducing e) f) ⁻¹' d
[PROOFSTEP]
exact hs_comp ⟨f a, ha₂, ⟨f b, this, hb₂⟩⟩


[GOAL]
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
⊢ 𝓝 0 = ⨅ (γ : Γ₀) (_ : γ ≠ 0), 𝓟 (Iio γ)
[PROOFSTEP]
rw [nhds_eq_update, update_same]
[GOAL]
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
⊢ HasBasis (𝓝 0) (fun γ => γ ≠ 0) Iio
[PROOFSTEP]
rw [nhds_zero]
[GOAL]
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
⊢ HasBasis (⨅ (γ : Γ₀) (_ : γ ≠ 0), 𝓟 (Iio γ)) (fun γ => γ ≠ 0) Iio
[PROOFSTEP]
refine' hasBasis_biInf_principal _ ⟨1, one_ne_zero⟩
[GOAL]
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
⊢ DirectedOn ((fun γ => Iio γ) ⁻¹'o fun x x_1 => x ≥ x_1) fun γ => γ = 0 → False
[PROOFSTEP]
exact directedOn_iff_directed.2 (directed_of_inf fun a b hab => Iio_subset_Iio hab)
[GOAL]
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
⊢ Tendsto f l (𝓝 0) ↔ ∀ (γ₀ : Γ₀), γ₀ ≠ 0 → ∀ᶠ (x : α) in l, f x < γ₀
[PROOFSTEP]
simp [nhds_zero]
[GOAL]
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ✝ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
γ : Γ₀
h₀ : γ ≠ 0
⊢ 𝓝 γ = pure γ
[PROOFSTEP]
rw [nhds_eq_update, update_noteq h₀]
[GOAL]
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ✝ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
γ : Γ₀ˣ
⊢ {↑γ} ∈ 𝓝 ↑γ
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
h : γ ≠ 0
⊢ {γ} ∈ 𝓝 γ
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
x : Γ₀
h : x ≠ 0
⊢ HasBasis (𝓝 x) (fun x => True) fun x_1 => {x}
[PROOFSTEP]
rw [nhds_of_ne_zero h]
[GOAL]
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
x : Γ₀
h : x ≠ 0
⊢ HasBasis (pure x) (fun x => True) fun x_1 => {x}
[PROOFSTEP]
exact hasBasis_pure _
[GOAL]
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ✝ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
γ : Γ₀
h : γ ≠ 0
⊢ Tendsto f l (𝓝 γ) ↔ ∀ᶠ (x : α) in l, f x = γ
[PROOFSTEP]
rw [nhds_of_ne_zero h, tendsto_pure]
[GOAL]
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
h : γ₁ < γ₂
⊢ Iio γ₂ ∈ 𝓝 γ₁
[PROOFSTEP]
rcases eq_or_ne γ₁ 0 with (rfl | h₀)
[GOAL]
case inl
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
h : 0 < γ₂
⊢ Iio γ₂ ∈ 𝓝 0
[PROOFSTEP]
simp [*, h.ne', Iio_mem_nhds_zero]
[GOAL]
case inr
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
h : γ₁ < γ₂
h₀ : γ₁ ≠ 0
⊢ Iio γ₂ ∈ 𝓝 γ₁
[PROOFSTEP]
simp [*, h.ne', Iio_mem_nhds_zero]
[GOAL]
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
s : Set Γ₀
⊢ IsOpen s ↔ ¬0 ∈ s ∨ ∃ γ, γ ≠ 0 ∧ Iio γ ⊆ s
[PROOFSTEP]
rw [isOpen_iff_mem_nhds, ← and_forall_ne (0 : Γ₀)]
[GOAL]
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
s : Set Γ₀
⊢ ((0 ∈ s → s ∈ 𝓝 0) ∧ ∀ (b : Γ₀), b ≠ 0 → b ∈ s → s ∈ 𝓝 b) ↔ ¬0 ∈ s ∨ ∃ γ, γ ≠ 0 ∧ Iio γ ⊆ s
[PROOFSTEP]
simp (config := { contextual := true }) [nhds_of_ne_zero, imp_iff_not_or, hasBasis_nhds_zero.mem_iff]
[GOAL]
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
s : Set Γ₀
⊢ IsClosed s ↔ 0 ∈ s ∨ ∃ γ, γ ≠ 0 ∧ s ⊆ Ici γ
[PROOFSTEP]
simp only [← isOpen_compl_iff, isOpen_iff, mem_compl_iff, not_not, ← compl_Ici, compl_subset_compl]
[GOAL]
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
⊢ IsClosed {p | p.fst ≤ p.snd}
[PROOFSTEP]
simp only [← isOpen_compl_iff, compl_setOf, not_le, isOpen_iff_mem_nhds]
[GOAL]
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
⊢ ∀ (a : Γ₀ × Γ₀), a ∈ {a | a.snd < a.fst} → {a | a.snd < a.fst} ∈ 𝓝 a
[PROOFSTEP]
rintro ⟨a, b⟩ (hab : b < a)
[GOAL]
case mk
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
a b : Γ₀
hab : b < a
⊢ {a | a.snd < a.fst} ∈ 𝓝 (a, b)
[PROOFSTEP]
rw [nhds_prod_eq, nhds_of_ne_zero (zero_le'.trans_lt hab).ne', pure_prod]
[GOAL]
case mk
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
a b : Γ₀
hab : b < a
⊢ {a | a.snd < a.fst} ∈ map (Prod.mk a) (𝓝 b)
[PROOFSTEP]
exact Iio_mem_nhds hab
[GOAL]
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
s t : Set Γ₀
h₁ : Disjoint (closure s) t
h₂ : Disjoint s (closure t)
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)
[PROOFSTEP]
by_cases hs : 0 ∈ s
[GOAL]
case pos
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
s t : Set Γ₀
h₁ : Disjoint (closure s) t
h₂ : Disjoint s (closure t)
hs : 0 ∈ s
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)
[PROOFSTEP]
have ht : 0 ∉ t := fun ht => disjoint_left.1 h₁ (subset_closure hs) ht
[GOAL]
case pos
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
s t : Set Γ₀
h₁ : Disjoint (closure s) t
h₂ : Disjoint s (closure t)
hs : 0 ∈ s
ht : ¬0 ∈ t
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)
[PROOFSTEP]
rwa [(isOpen_iff.2 (.inl ht)).nhdsSet_eq, disjoint_nhdsSet_principal]
[GOAL]
case neg
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
s t : Set Γ₀
h₁ : Disjoint (closure s) t
h₂ : Disjoint s (closure t)
hs : ¬0 ∈ s
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)
[PROOFSTEP]
rwa [(isOpen_iff.2 (.inl hs)).nhdsSet_eq, disjoint_principal_nhdsSet]
[GOAL]
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
⊢ Continuous fun p => p.fst * p.snd
[PROOFSTEP]
simp only [continuous_iff_continuousAt, ContinuousAt]
[GOAL]
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
⊢ ∀ (x : Γ₀ × Γ₀), Tendsto (fun p => p.fst * p.snd) (𝓝 x) (𝓝 (x.fst * x.snd))
[PROOFSTEP]
rintro ⟨x, y⟩
[GOAL]
case mk
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
x y : Γ₀
⊢ Tendsto (fun p => p.fst * p.snd) (𝓝 (x, y)) (𝓝 ((x, y).fst * (x, y).snd))
[PROOFSTEP]
wlog hle : x ≤ y generalizing x y
[GOAL]
case mk.inr
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
x y : Γ₀
this : ∀ (x y : Γ₀), x ≤ y → Tendsto (fun p => p.fst * p.snd) (𝓝 (x, y)) (𝓝 ((x, y).fst * (x, y).snd))
hle : ¬x ≤ y
⊢ Tendsto (fun p => p.fst * p.snd) (𝓝 (x, y)) (𝓝 ((x, y).fst * (x, y).snd))
[PROOFSTEP]
have := (this y x (le_of_not_le hle)).comp (continuous_swap.tendsto (x, y))
[GOAL]
case mk.inr
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
x y : Γ₀
this✝ : ∀ (x y : Γ₀), x ≤ y → Tendsto (fun p => p.fst * p.snd) (𝓝 (x, y)) (𝓝 ((x, y).fst * (x, y).snd))
hle : ¬x ≤ y
this : Tendsto ((fun p => p.fst * p.snd) ∘ Prod.swap) (𝓝 (x, y)) (𝓝 ((y, x).fst * (y, x).snd))
⊢ Tendsto (fun p => p.fst * p.snd) (𝓝 (x, y)) (𝓝 ((x, y).fst * (x, y).snd))
[PROOFSTEP]
simpa only [mul_comm, Function.comp, Prod.swap] using this
[GOAL]
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
x y : Γ₀
hle : x ≤ y
⊢ Tendsto (fun p => p.fst * p.snd) (𝓝 (x, y)) (𝓝 ((x, y).fst * (x, y).snd))
[PROOFSTEP]
rcases eq_or_ne x 0 with (rfl | hx) <;> [rcases eq_or_ne y 0 with (rfl | hy); skip]
[GOAL]
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
x y : Γ₀
hle : x ≤ y
⊢ Tendsto (fun p => p.fst * p.snd) (𝓝 (x, y)) (𝓝 ((x, y).fst * (x, y).snd))
[PROOFSTEP]
rcases eq_or_ne x 0 with (rfl | hx)
[GOAL]
case inl
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
y : Γ₀
hle : 0 ≤ y
⊢ Tendsto (fun p => p.fst * p.snd) (𝓝 (0, y)) (𝓝 ((0, y).fst * (0, y).snd))
[PROOFSTEP]
rcases eq_or_ne y 0 with (rfl | hy)
[GOAL]
case inr
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
x y : Γ₀
hle : x ≤ y
hx : x ≠ 0
⊢ Tendsto (fun p => p.fst * p.snd) (𝓝 (x, y)) (𝓝 ((x, y).fst * (x, y).snd))
[PROOFSTEP]
skip
[GOAL]
case inl.inl
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
hle : 0 ≤ 0
⊢ Tendsto (fun p => p.fst * p.snd) (𝓝 (0, 0)) (𝓝 ((0, 0).fst * (0, 0).snd))
[PROOFSTEP]
rw [zero_mul]
[GOAL]
case inl.inl
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
hle : 0 ≤ 0
⊢ Tendsto (fun p => p.fst * p.snd) (𝓝 (0, 0)) (𝓝 0)
[PROOFSTEP]
refine
  ((hasBasis_nhds_zero.prod_nhds hasBasis_nhds_zero).tendsto_iff hasBasis_nhds_zero).2 fun γ hγ =>
    ⟨(γ, 1), ⟨hγ, one_ne_zero⟩, ?_⟩
[GOAL]
case inl.inl
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ✝ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
hle : 0 ≤ 0
γ : Γ₀
hγ : γ ≠ 0
⊢ ∀ (x : Γ₀ × Γ₀), x ∈ Iio (γ, 1).fst ×ˢ Iio (γ, 1).snd → x.fst * x.snd ∈ Iio γ
[PROOFSTEP]
rintro ⟨x, y⟩ ⟨hx : x < γ, hy : y < 1⟩
[GOAL]
case inl.inl.mk.intro
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ✝ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
hle : 0 ≤ 0
γ : Γ₀
hγ : γ ≠ 0
x y : Γ₀
hx : x < γ
hy : y < 1
⊢ (x, y).fst * (x, y).snd ∈ Iio γ
[PROOFSTEP]
exact (mul_lt_mul₀ hx hy).trans_eq (mul_one γ)
[GOAL]
case inl.inr
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
y : Γ₀
hle : 0 ≤ y
hy : y ≠ 0
⊢ Tendsto (fun p => p.fst * p.snd) (𝓝 (0, y)) (𝓝 ((0, y).fst * (0, y).snd))
[PROOFSTEP]
rw [zero_mul, nhds_prod_eq, nhds_of_ne_zero hy, prod_pure, tendsto_map'_iff]
[GOAL]
case inl.inr
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
y : Γ₀
hle : 0 ≤ y
hy : y ≠ 0
⊢ Tendsto ((fun p => p.fst * p.snd) ∘ fun a => (a, y)) (𝓝 0) (𝓝 0)
[PROOFSTEP]
refine' (hasBasis_nhds_zero.tendsto_iff hasBasis_nhds_zero).2 fun γ hγ => _
[GOAL]
case inl.inr
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ✝ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
y : Γ₀
hle : 0 ≤ y
hy : y ≠ 0
γ : Γ₀
hγ : γ ≠ 0
⊢ ∃ ia, ia ≠ 0 ∧ ∀ (x : Γ₀), x ∈ Iio ia → ((fun p => p.fst * p.snd) ∘ fun a => (a, y)) x ∈ Iio γ
[PROOFSTEP]
refine' ⟨γ / y, div_ne_zero hγ hy, fun x hx => _⟩
[GOAL]
case inl.inr
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ✝ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
y : Γ₀
hle : 0 ≤ y
hy : y ≠ 0
γ : Γ₀
hγ : γ ≠ 0
x : Γ₀
hx : x ∈ Iio (γ / y)
⊢ ((fun p => p.fst * p.snd) ∘ fun a => (a, y)) x ∈ Iio γ
[PROOFSTEP]
calc
  x * y < γ / y * y := mul_lt_right₀ _ hx hy
  _ = γ := div_mul_cancel _ hy
[GOAL]
case inr
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
x y : Γ₀
hle : x ≤ y
hx : x ≠ 0
⊢ Tendsto (fun p => p.fst * p.snd) (𝓝 (x, y)) (𝓝 ((x, y).fst * (x, y).snd))
[PROOFSTEP]
have hy : y ≠ 0 := ((zero_lt_iff.mpr hx).trans_le hle).ne'
[GOAL]
case inr
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
x y : Γ₀
hle : x ≤ y
hx : x ≠ 0
hy : y ≠ 0
⊢ Tendsto (fun p => p.fst * p.snd) (𝓝 (x, y)) (𝓝 ((x, y).fst * (x, y).snd))
[PROOFSTEP]
rw [nhds_prod_eq, nhds_of_ne_zero hx, nhds_of_ne_zero hy, prod_pure_pure]
[GOAL]
case inr
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
x y : Γ₀
hle : x ≤ y
hx : x ≠ 0
hy : y ≠ 0
⊢ Tendsto (fun p => p.fst * p.snd) (pure (x, y)) (𝓝 ((x, y).fst * (x, y).snd))
[PROOFSTEP]
exact pure_le_nhds (x * y)
[GOAL]
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ✝ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
γ : Γ₀
h : γ ≠ 0
⊢ ContinuousAt Inv.inv γ
[PROOFSTEP]
rw [ContinuousAt, nhds_of_ne_zero h]
[GOAL]
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ✝ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
γ : Γ₀
h : γ ≠ 0
⊢ Tendsto Inv.inv (pure γ) (𝓝 γ⁻¹)
[PROOFSTEP]
exact pure_le_nhds γ⁻¹