isOpen_B_with_param — Mathlib

English

The measurable set of differentiableAt with parameter is measurable when K is complete.

Русский

Измеримое множество дифференцируемости с параметром измеримо при полном K.

LaTeX

$$MeasurableSet {p : α × E | DifferentiableAt 𝕜 (f p.fst) p.snd ∧ fderiv 𝕜 (f p.fst) p.snd ∈ K}$$

Lean4

theorem isOpen_B_with_param {r s t : ℝ} (hf : Continuous f.uncurry) (K : Set (E →L[𝕜] F)) :
    IsOpen {p : α × E | p.2 ∈ B (f p.1) K r s t} :=
  by
  suffices H : IsOpen (⋃ L ∈ K, {p : α × E | p.2 ∈ A (f p.1) L r t ∧ p.2 ∈ A (f p.1) L s t}) by convert H; ext p;
    simp [B]
  refine isOpen_biUnion (fun L _ ↦ ?_)
  exact (isOpen_A_with_param hf L).inter (isOpen_A_with_param hf L)

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