α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.93600
inst✝ : UniformSpace α
⊢ HasBasis (𝓤 α) (fun V => (V ∈ 𝓤 α ∧ IsOpen V) ∧ SymmetricRel V) id
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.93600
inst✝ : UniformSpace α
⊢ HasBasis (𝓤 α) (fun V => V ∈ 𝓤 α ∧ IsOpen V ∧ SymmetricRel V) id
simp only [← and_assoc]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.93600
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α ∧ IsOpen s
⊢ (symmetrizeRel s ∈ 𝓤 α ∧ IsOpen (symmetrizeRel s)) ∧ SymmetricRel (symmetrizeRel s) ∧ id (symmetrizeRel s) ⊆ id s
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.93600
inst✝ : UniformSpace α
⊢ HasBasis (𝓤 α) (fun V => (V ∈ 𝓤 α ∧ IsOpen V) ∧ SymmetricRel V) id
refine' uniformity_hasBasis_open.restrict fun s hs => ⟨symmetrizeRel s, _⟩
no goals
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.93600
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α ∧ IsOpen s
⊢ (symmetrizeRel s ∈ 𝓤 α ∧ IsOpen (symmetrizeRel s)) ∧ SymmetricRel (symmetrizeRel s) ∧ id (symmetrizeRel s) ⊆ id s
exact
  ⟨⟨symmetrize_mem_uniformity hs.1, IsOpen.inter hs.2 (hs.2.preimage continuous_swap)⟩,
    symmetric_symmetrizeRel s, symmetrizeRel_subset_self s⟩