case intro.intro
α : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
ι : Type u_1
inst✝ : SeparatedSpace α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
f : ι → α
hf : Pairwise fun x y => ¬(f x, f y) ∈ V₀
x y : ι
h : f x ≠ f y
⊢ ¬(f x, f y) ∈ V₀
α : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
ι : Type u_1
inst✝ : SeparatedSpace α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
f : ι → α
hf : Pairwise fun x y => ¬(f x, f y) ∈ V₀
⊢ Set.Pairwise (range f) fun x y => ¬(x, y) ∈ V₀
rintro _ ⟨x, rfl⟩ _ ⟨y, rfl⟩ h
no goals
case intro.intro
α : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
ι : Type u_1
inst✝ : SeparatedSpace α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
f : ι → α
hf : Pairwise fun x y => ¬(f x, f y) ∈ V₀
x y : ι
h : f x ≠ f y
⊢ ¬(f x, f y) ∈ V₀
exact hf (ne_of_apply_ne f h)