case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.44329
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
x : β
h_cont : Continuous f
hx : Tendsto f (cocompact α) (𝓝 x)
r : Set (β × β)
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SymmetricRel t
htr : t ○ t ⊆ r
⊢ {x | (f x.fst, f x.snd) ∈ r} ∈ 𝓤 α
α : Type u_1
β : Type u_2
γ : Type ?u.44329
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
x : β
h_cont : Continuous f
hx : Tendsto f (cocompact α) (𝓝 x)
r : Set (β × β)
hr : r ∈ 𝓤 β
⊢ {x | (f x.fst, f x.snd) ∈ r} ∈ 𝓤 α
obtain ⟨t, ht, htsymm, htr⟩ := comp_symm_mem_uniformity_sets hr
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.44329
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
x : β
h_cont : Continuous f
hx : Tendsto f (cocompact α) (𝓝 x)
r : Set (β × β)
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SymmetricRel t
htr : t ○ t ⊆ r
s : Set α
hs : IsCompact s
hst : sᶜ ⊆ f ⁻¹' {y | (x, y) ∈ t}
⊢ {x | (f x.fst, f x.snd) ∈ r} ∈ 𝓤 α
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.44329
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
x : β
h_cont : Continuous f
hx : Tendsto f (cocompact α) (𝓝 x)
r : Set (β × β)
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SymmetricRel t
htr : t ○ t ⊆ r
⊢ {x | (f x.fst, f x.snd) ∈ r} ∈ 𝓤 α
obtain ⟨s, hs, hst⟩ := mem_cocompact.1 (hx <| mem_nhds_left _ ht)
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.44329
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
x : β
h_cont : Continuous f
hx : Tendsto f (cocompact α) (𝓝 x)
r : Set (β × β)
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SymmetricRel t
htr : t ○ t ⊆ r
s : Set α
hs : IsCompact s
hst : sᶜ ⊆ f ⁻¹' {y | (x, y) ∈ t}
⊢ symmetrizeRel {x | x.fst ∈ s → (f x.fst, f x.snd) ∈ symmetrizeRel r} ⊆ {x | (f x.fst, f x.snd) ∈ r}
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.44329
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
x : β
h_cont : Continuous f
hx : Tendsto f (cocompact α) (𝓝 x)
r : Set (β × β)
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SymmetricRel t
htr : t ○ t ⊆ r
s : Set α
hs : IsCompact s
hst : sᶜ ⊆ f ⁻¹' {y | (x, y) ∈ t}
⊢ {x | (f x.fst, f x.snd) ∈ r} ∈ 𝓤 α
apply
  mem_of_superset
    (symmetrize_mem_uniformity <|
      (hs.uniformContinuousAt_of_continuousAt f fun _ _ => h_cont.continuousAt) <|
        symmetrize_mem_uniformity hr)
case intro.intro.intro.intro.intro.mk
α : Type u_1
β : Type u_2
γ : Type ?u.44329
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
x : β
h_cont : Continuous f
hx : Tendsto f (cocompact α) (𝓝 x)
r : Set (β × β)
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SymmetricRel t
htr : t ○ t ⊆ r
s : Set α
hs : IsCompact s
hst : sᶜ ⊆ f ⁻¹' {y | (x, y) ∈ t}
b₁ b₂ : α
h : (b₁, b₂) ∈ symmetrizeRel {x | x.fst ∈ s → (f x.fst, f x.snd) ∈ symmetrizeRel r}
⊢ (b₁, b₂) ∈ {x | (f x.fst, f x.snd) ∈ r}
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.44329
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
x : β
h_cont : Continuous f
hx : Tendsto f (cocompact α) (𝓝 x)
r : Set (β × β)
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SymmetricRel t
htr : t ○ t ⊆ r
s : Set α
hs : IsCompact s
hst : sᶜ ⊆ f ⁻¹' {y | (x, y) ∈ t}
⊢ symmetrizeRel {x | x.fst ∈ s → (f x.fst, f x.snd) ∈ symmetrizeRel r} ⊆ {x | (f x.fst, f x.snd) ∈ r}
rintro ⟨b₁, b₂⟩ h
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.44329
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
x : β
h_cont : Continuous f
hx : Tendsto f (cocompact α) (𝓝 x)
r : Set (β × β)
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SymmetricRel t
htr : t ○ t ⊆ r
s : Set α
hs : IsCompact s
hst : sᶜ ⊆ f ⁻¹' {y | (x, y) ∈ t}
b₁ b₂ : α
h : (b₁, b₂) ∈ symmetrizeRel {x | x.fst ∈ s → (f x.fst, f x.snd) ∈ symmetrizeRel r}
h₁ : b₁ ∈ s
⊢ (b₁, b₂) ∈ {x | (f x.fst, f x.snd) ∈ r}

case neg
α : Type u_1
β : Type u_2
γ : Type ?u.44329
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
x : β
h_cont : Continuous f
hx : Tendsto f (cocompact α) (𝓝 x)
r : Set (β × β)
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SymmetricRel t
htr : t ○ t ⊆ r
s : Set α
hs : IsCompact s
hst : sᶜ ⊆ f ⁻¹' {y | (x, y) ∈ t}
b₁ b₂ : α
h : (b₁, b₂) ∈ symmetrizeRel {x | x.fst ∈ s → (f x.fst, f x.snd) ∈ symmetrizeRel r}
h₁ : ¬b₁ ∈ s
⊢ (b₁, b₂) ∈ {x | (f x.fst, f x.snd) ∈ r}
case intro.intro.intro.intro.intro.mk
α : Type u_1
β : Type u_2
γ : Type ?u.44329
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
x : β
h_cont : Continuous f
hx : Tendsto f (cocompact α) (𝓝 x)
r : Set (β × β)
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SymmetricRel t
htr : t ○ t ⊆ r
s : Set α
hs : IsCompact s
hst : sᶜ ⊆ f ⁻¹' {y | (x, y) ∈ t}
b₁ b₂ : α
h : (b₁, b₂) ∈ symmetrizeRel {x | x.fst ∈ s → (f x.fst, f x.snd) ∈ symmetrizeRel r}
⊢ (b₁, b₂) ∈ {x | (f x.fst, f x.snd) ∈ r}
by_cases h₁ : b₁ ∈ s
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.44329
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
x : β
h_cont : Continuous f
hx : Tendsto f (cocompact α) (𝓝 x)
r : Set (β × β)
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SymmetricRel t
htr : t ○ t ⊆ r
s : Set α
hs : IsCompact s
hst : sᶜ ⊆ f ⁻¹' {y | (x, y) ∈ t}
b₁ b₂ : α
h : (b₁, b₂) ∈ symmetrizeRel {x | x.fst ∈ s → (f x.fst, f x.snd) ∈ symmetrizeRel r}
h₁ : ¬b₁ ∈ s
h₂ : b₂ ∈ s
⊢ (b₁, b₂) ∈ {x | (f x.fst, f x.snd) ∈ r}

case neg
α : Type u_1
β : Type u_2
γ : Type ?u.44329
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
x : β
h_cont : Continuous f
hx : Tendsto f (cocompact α) (𝓝 x)
r : Set (β × β)
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SymmetricRel t
htr : t ○ t ⊆ r
s : Set α
hs : IsCompact s
hst : sᶜ ⊆ f ⁻¹' {y | (x, y) ∈ t}
b₁ b₂ : α
h : (b₁, b₂) ∈ symmetrizeRel {x | x.fst ∈ s → (f x.fst, f x.snd) ∈ symmetrizeRel r}
h₁ : ¬b₁ ∈ s
h₂ : ¬b₂ ∈ s
⊢ (b₁, b₂) ∈ {x | (f x.fst, f x.snd) ∈ r}
case neg
α : Type u_1
β : Type u_2
γ : Type ?u.44329
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
x : β
h_cont : Continuous f
hx : Tendsto f (cocompact α) (𝓝 x)
r : Set (β × β)
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SymmetricRel t
htr : t ○ t ⊆ r
s : Set α
hs : IsCompact s
hst : sᶜ ⊆ f ⁻¹' {y | (x, y) ∈ t}
b₁ b₂ : α
h : (b₁, b₂) ∈ symmetrizeRel {x | x.fst ∈ s → (f x.fst, f x.snd) ∈ symmetrizeRel r}
h₁ : ¬b₁ ∈ s
⊢ (b₁, b₂) ∈ {x | (f x.fst, f x.snd) ∈ r}
by_cases h₂ : b₂ ∈ s
case neg.a
α : Type u_1
β : Type u_2
γ : Type ?u.44329
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
x : β
h_cont : Continuous f
hx : Tendsto f (cocompact α) (𝓝 x)
r : Set (β × β)
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SymmetricRel t
htr : t ○ t ⊆ r
s : Set α
hs : IsCompact s
hst : sᶜ ⊆ f ⁻¹' {y | (x, y) ∈ t}
b₁ b₂ : α
h : (b₁, b₂) ∈ symmetrizeRel {x | x.fst ∈ s → (f x.fst, f x.snd) ∈ symmetrizeRel r}
h₁ : ¬b₁ ∈ s
h₂ : ¬b₂ ∈ s
⊢ (f (b₁, b₂).fst, f (b₁, b₂).snd) ∈ t ○ t
case neg
α : Type u_1
β : Type u_2
γ : Type ?u.44329
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
x : β
h_cont : Continuous f
hx : Tendsto f (cocompact α) (𝓝 x)
r : Set (β × β)
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SymmetricRel t
htr : t ○ t ⊆ r
s : Set α
hs : IsCompact s
hst : sᶜ ⊆ f ⁻¹' {y | (x, y) ∈ t}
b₁ b₂ : α
h : (b₁, b₂) ∈ symmetrizeRel {x | x.fst ∈ s → (f x.fst, f x.snd) ∈ symmetrizeRel r}
h₁ : ¬b₁ ∈ s
h₂ : ¬b₂ ∈ s
⊢ (b₁, b₂) ∈ {x | (f x.fst, f x.snd) ∈ r}
apply htr
no goals
case neg.a
α : Type u_1
β : Type u_2
γ : Type ?u.44329
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
x : β
h_cont : Continuous f
hx : Tendsto f (cocompact α) (𝓝 x)
r : Set (β × β)
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SymmetricRel t
htr : t ○ t ⊆ r
s : Set α
hs : IsCompact s
hst : sᶜ ⊆ f ⁻¹' {y | (x, y) ∈ t}
b₁ b₂ : α
h : (b₁, b₂) ∈ symmetrizeRel {x | x.fst ∈ s → (f x.fst, f x.snd) ∈ symmetrizeRel r}
h₁ : ¬b₁ ∈ s
h₂ : ¬b₂ ∈ s
⊢ (f (b₁, b₂).fst, f (b₁, b₂).snd) ∈ t ○ t
exact ⟨x, htsymm.mk_mem_comm.1 (hst h₁), hst h₂⟩
no goals
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.44329
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
x : β
h_cont : Continuous f
hx : Tendsto f (cocompact α) (𝓝 x)
r : Set (β × β)
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SymmetricRel t
htr : t ○ t ⊆ r
s : Set α
hs : IsCompact s
hst : sᶜ ⊆ f ⁻¹' {y | (x, y) ∈ t}
b₁ b₂ : α
h : (b₁, b₂) ∈ symmetrizeRel {x | x.fst ∈ s → (f x.fst, f x.snd) ∈ symmetrizeRel r}
h₁ : b₁ ∈ s
⊢ (b₁, b₂) ∈ {x | (f x.fst, f x.snd) ∈ r}
exact (h.1 h₁).1
no goals
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.44329
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
x : β
h_cont : Continuous f
hx : Tendsto f (cocompact α) (𝓝 x)
r : Set (β × β)
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SymmetricRel t
htr : t ○ t ⊆ r
s : Set α
hs : IsCompact s
hst : sᶜ ⊆ f ⁻¹' {y | (x, y) ∈ t}
b₁ b₂ : α
h : (b₁, b₂) ∈ symmetrizeRel {x | x.fst ∈ s → (f x.fst, f x.snd) ∈ symmetrizeRel r}
h₁ : ¬b₁ ∈ s
h₂ : b₂ ∈ s
⊢ (b₁, b₂) ∈ {x | (f x.fst, f x.snd) ∈ r}
exact (h.2 h₂).2