isOpen_B

Mathlib.Analysis.Calculus.FDeriv.Measurable

URI: https://scilib.ai/kg/mathlib#FDerivMeasurableAux.isOpen_B

English

Simp lemma: A is open under standard topological assumptions.

Русский

Лемма-сокращение: A открыто при стандартных предположениях о топологии.

LaTeX

$$$$\text{IsOpen}(A(f,L,r,\varepsilon))\ \text{(simplified)}.$$$$

Lean4

theorem isOpen_B {K : Set (E →L[𝕜] F)} {r s ε : ℝ} : IsOpen (B f K r s ε) := by
  simp [B, isOpen_biUnion, IsOpen.inter, isOpen_A]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru