English
With HasBasis bases on α and β, IsUniformEmbedding f is equivalent to a pair of bounds expressed via basis elements and f’s action on products.
Русский
С базисами HasBasis для α и β, IsUniformEmbedding f эквивалентно паре ограничений через базис и действия f на произведениях.
LaTeX
$$$IsUniformEmbedding f \\iff Injective f \\land (∀ i, p' i → ∃ j, p j ∧ ∀ x y, (x, y) ∈ s j → (f x, f y) ∈ s' i) ∧ (∀ j, p j → ∃ i, p' i ∧ ∀ x y, (f x, f y) ∈ s' i → (x, y) ∈ s j)$$$
Lean4
theorem isUniformEmbedding_iff' {ι ι'} {p : ι → Prop} {p' : ι' → Prop} {s s'} (h : (𝓤 α).HasBasis p s)
(h' : (𝓤 β).HasBasis p' s') {f : α → β} :
IsUniformEmbedding f ↔
Injective f ∧
(∀ i, p' i → ∃ j, p j ∧ ∀ x y, (x, y) ∈ s j → (f x, f y) ∈ s' i) ∧
(∀ j, p j → ∃ i, p' i ∧ ∀ x y, (f x, f y) ∈ s' i → (x, y) ∈ s j) :=
by rw [isUniformEmbedding_iff, and_comm, h.isUniformInducing_iff h']
