congr_set — Mathlib

English

If s and t are nhds-equivalent near x, then a local property P preserved under nhds equivalence holds for s and t together with f.

Русский

Если области s и t совпадают в окрестности x по отношению к гиперплоскости, то свойство P сохраняется для обеих областей совместно с f.

LaTeX

$$$G.LocalInvariantProp P \Rightarrow P f s x \iff P f t x \text{ whenever } s \equiv_{\mathcal{N}x} t$$$

Lean4

theorem congr_set {s t : Set H} {x : H} {f : H → H'} (hu : s =ᶠ[𝓝 x] t) : P f s x ↔ P f t x :=
  by
  obtain ⟨o, host, ho, hxo⟩ := mem_nhds_iff.mp hu.mem_iff
  simp_rw [subset_def, mem_setOf, ← and_congr_left_iff, ← mem_inter_iff, ← Set.ext_iff] at host
  rw [hG.is_local ho hxo, host, ← hG.is_local ho hxo]

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