case intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.53210
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
left✝ : SymmetricRel w
w_sub : w ○ w ⊆ s
⊢ ∃ t, t ∈ 𝓤 α ∧ SymmetricRel t ∧ t ○ t ○ t ⊆ s
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.53210
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ ∃ t, t ∈ 𝓤 α ∧ SymmetricRel t ∧ t ○ t ○ t ⊆ s
rcases comp_symm_mem_uniformity_sets hs with ⟨w, w_in, _, w_sub⟩
case intro.intro.intro.intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.53210
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
left✝ : SymmetricRel w
w_sub : w ○ w ⊆ s
t : Set (α × α)
t_in : t ∈ 𝓤 α
t_symm : SymmetricRel t
t_sub : t ○ t ⊆ w
⊢ ∃ t, t ∈ 𝓤 α ∧ SymmetricRel t ∧ t ○ t ○ t ⊆ s
case intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.53210
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
left✝ : SymmetricRel w
w_sub : w ○ w ⊆ s
⊢ ∃ t, t ∈ 𝓤 α ∧ SymmetricRel t ∧ t ○ t ○ t ⊆ s
rcases comp_symm_mem_uniformity_sets w_in with ⟨t, t_in, t_symm, t_sub⟩
case intro.intro.intro.intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.53210
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
left✝ : SymmetricRel w
w_sub : w ○ w ⊆ s
t : Set (α × α)
t_in : t ∈ 𝓤 α
t_symm : SymmetricRel t
t_sub : t ○ t ⊆ w
⊢ t ○ t ○ t ⊆ s
case intro.intro.intro.intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.53210
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
left✝ : SymmetricRel w
w_sub : w ○ w ⊆ s
t : Set (α × α)
t_in : t ∈ 𝓤 α
t_symm : SymmetricRel t
t_sub : t ○ t ⊆ w
⊢ ∃ t, t ∈ 𝓤 α ∧ SymmetricRel t ∧ t ○ t ○ t ⊆ s
use t, t_in, t_symm
case intro.intro.intro.intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.53210
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
left✝ : SymmetricRel w
w_sub : w ○ w ⊆ s
t : Set (α × α)
t_in : t ∈ 𝓤 α
t_symm : SymmetricRel t
t_sub : t ○ t ⊆ w
this : t ⊆ t ○ t
⊢ t ○ t ○ t ⊆ s
case intro.intro.intro.intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.53210
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
left✝ : SymmetricRel w
w_sub : w ○ w ⊆ s
t : Set (α × α)
t_in : t ∈ 𝓤 α
t_symm : SymmetricRel t
t_sub : t ○ t ⊆ w
⊢ t ○ t ○ t ⊆ s
have : t ⊆ t ○ t := subset_comp_self_of_mem_uniformity t_in
no goals
case intro.intro.intro.intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.53210
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
left✝ : SymmetricRel w
w_sub : w ○ w ⊆ s
t : Set (α × α)
t_in : t ∈ 𝓤 α
t_symm : SymmetricRel t
t_sub : t ○ t ⊆ w
this : t ⊆ t ○ t
⊢ t ○ t ○ t ⊆ s
calc
  t ○ t ○ t ⊆ w ○ t := compRel_mono t_sub Subset.rfl
  _ ⊆ w ○ (t ○ t) := compRel_mono Subset.rfl this
  _ ⊆ w ○ w := compRel_mono Subset.rfl t_sub
  _ ⊆ s := w_sub