case intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.52621
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_sub : w ○ w ⊆ s
⊢ ∃ t, t ∈ 𝓤 α ∧ SymmetricRel t ∧ t ○ t ⊆ s
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.52621
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ ∃ t, t ∈ 𝓤 α ∧ SymmetricRel t ∧ t ○ t ⊆ s
obtain ⟨w, w_in, w_sub⟩ : ∃ w ∈ 𝓤 α, w ○ w ⊆ s := comp_mem_uniformity_sets hs
case intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.52621
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_sub : w ○ w ⊆ s
⊢ symmetrizeRel w ○ symmetrizeRel w ⊆ s
case intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.52621
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_sub : w ○ w ⊆ s
⊢ ∃ t, t ∈ 𝓤 α ∧ SymmetricRel t ∧ t ○ t ⊆ s
use symmetrizeRel w, symmetrize_mem_uniformity w_in, symmetric_symmetrizeRel w
case intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.52621
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_sub : w ○ w ⊆ s
this : symmetrizeRel w ⊆ w
⊢ symmetrizeRel w ○ symmetrizeRel w ⊆ s
case intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.52621
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_sub : w ○ w ⊆ s
⊢ symmetrizeRel w ○ symmetrizeRel w ⊆ s
have : symmetrizeRel w ⊆ w := symmetrizeRel_subset_self w
no goals
case intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.52621
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_sub : w ○ w ⊆ s
this : symmetrizeRel w ⊆ w
⊢ symmetrizeRel w ○ symmetrizeRel w ⊆ s
exact (compRel_mono this this).trans w_sub