uniformContinuous_uncurry_lift₂

English

For a family h that preserves inseparability, uniform continuity of uncurry (lift₂ f h) is equivalent to uniform continuity of uncurry f.

Русский

Для семейства h, сохраняющего неразделимость, равномерная непрерывность uncurry (lift₂ f h) эквивалентна равномерной непрерывности uncurry f.

LaTeX

$$$UniformContinuous\ (uncurry \lvert lift₂\ f\ h) \iff UniformContinuous\ (uncurry\ f)$$$

Lean4

theorem uniformContinuous_uncurry_lift₂ {f : α → β → γ}
    (h : ∀ a c b d, Inseparable a b → Inseparable c d → f a c = f b d) :
    UniformContinuous (uncurry <| lift₂ f h) ↔ UniformContinuous (uncurry f) :=
  uniformContinuous_dom₂

Похожие утверждения