lift₂_mk — Mathlib

English

Tendsto (uncurry (lift₂ f hf)) (nhds (mk x, mk y)) l ↔ Tendsto (uncurry f) (nhds (x, y)) l.

Русский

Tendsto (uncurry (lift₂ f hf)) (nhds (mk x, mk y)) l ⇔ Tendsto (uncurry f) (nhds (x, y)) l.

LaTeX

$$Tendsto (uncurry <| lift₂ f hf) (nhds (mk x, mk y)) l ↔ Tendsto (uncurry f) (nhds (x, y)) l$$

Lean4

@[simp]
theorem lift₂_mk {f : X → Y → α} (hf : ∀ a b c d, (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d) (x : X) (y : Y) :
    lift₂ f hf (mk x) (mk y) = f x y :=
  rfl

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