continuousWithinAt_prod_iff — Mathlib

English

A map into a product is continuous within s at x iff its components are continuous within s at x.

Русский

Отображение в произведение непрерывно внутри s в x тогда и только тогда, когда его компоненты непрерывны внутри s в x.

LaTeX

$$$\text{ContinuousWithinAt } f s x \iff \Big( \text{ContinuousWithinAt } (Prod.fst \circ f) s x \land \text{ContinuousWithinAt } (Prod.snd \circ f) s x \Big)$$$

Lean4

theorem continuousWithinAt_prod_iff {f : α → β × γ} {s : Set α} {x : α} :
    ContinuousWithinAt f s x ↔ ContinuousWithinAt (Prod.fst ∘ f) s x ∧ ContinuousWithinAt (Prod.snd ∘ f) s x :=
  ⟨fun h => ⟨h.fst, h.snd⟩, fun ⟨h1, h2⟩ => h1.prodMk h2⟩

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