uncurry_left — Mathlib

English

IsOpenMap f is equivalent to IsOpenMap of the left fibers for all a: IsOpenMap (λ x, f(a,x)).

Русский

IsOpenMap f эквивалентно IsOpenMap отображения a ↦ f(a,·) для каждого a.

LaTeX

$$$$\text{IsOpenMap } f \iff \forall a, \text{IsOpenMap }\bigl( x \mapsto f(a,x) \bigr). $$$$

Lean4

theorem uncurry_left {f : α → β → γ} {sα : Set α} {sβ : Set β} (a : α) (ha : a ∈ sα)
    (h : ContinuousOn f.uncurry (sα ×ˢ sβ)) : ContinuousOn (f a) sβ :=
  by
  let g : β → γ := f.uncurry ∘ (fun b => (a, b))
  refine ContinuousOn.congr (f := g) ?_ (fun y => by simp [g])
  exact ContinuousOn.comp h (by fun_prop) (by grind [Set.MapsTo])

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