α : Type u
β : Type v
X : Type ?u.199771
inst✝¹ : PseudoEMetricSpace α
x✝² y z : α
ε✝ ε₁ ε₂ : ℝ≥0∞
s t✝ : Set α
inst✝ : PseudoEMetricSpace β
f : α → β
t : Set β
a : α
b : β
ε : ℝ≥0∞
x✝¹ : 0 < ε
δ : ℝ≥0∞
x✝ : 0 < δ
x : α
⊢ edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t ↔ x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
α : Type u
β : Type v
X : Type ?u.199771
inst✝¹ : PseudoEMetricSpace α
x✝² y z : α
ε✝ ε₁ ε₂ : ℝ≥0∞
s t✝ : Set α
inst✝ : PseudoEMetricSpace β
f : α → β
t : Set β
a : α
b : β
ε : ℝ≥0∞
x✝¹ : 0 < ε
δ : ℝ≥0∞
x✝ : 0 < δ
x : α
⊢ x ∈ ball a δ ∩ s → f x ∈ ball b ε ∩ t ↔ x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
simp
no goals
α : Type u
β : Type v
X : Type ?u.199771
inst✝¹ : PseudoEMetricSpace α
x✝² y z : α
ε✝ ε₁ ε₂ : ℝ≥0∞
s t✝ : Set α
inst✝ : PseudoEMetricSpace β
f : α → β
t : Set β
a : α
b : β
ε : ℝ≥0∞
x✝¹ : 0 < ε
δ : ℝ≥0∞
x✝ : 0 < δ
x : α
⊢ edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t ↔ x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
tauto