mlieBracketWithin_inter — Mathlib

English

If t is a neighborhood of x, then bracketing over s ∩ t equals bracketing over s at x.

Русский

Если t является окрестностью x, то скобка внутри s ∩ t равна скобке внутри s в точке x.

LaTeX

$$$\mathrm{mlieBracketWithin}(I,V,W, s \cap t, x) = \mathrm{mlieBracketWithin}(I,V,W, s, x)$ for $t \in \mathcal{N}(x)$$$

Lean4

theorem mlieBracketWithin_inter (ht : t ∈ 𝓝 x) : mlieBracketWithin I V W (s ∩ t) x = mlieBracketWithin I V W s x :=
  by
  apply mlieBracketWithin_congr_set
  filter_upwards [ht] with y hy
  change (y ∈ s ∩ t) = (y ∈ s)
  simp_all

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