isOpen_eqLocus — Mathlib

English

If p is locally injective, and p ∘ g1 = p ∘ g2, then the set where g1 equals g2 is open.

Русский

Если p локально инъективна и p ∘ g1 = p ∘ g2, то множество {a | g1 a = g2 a} открыто.

LaTeX

$$IsLocallyInjective p → (p ∘ g1 = p ∘ g2) → IsOpen {a | g1 a = g2 a}$$

Lean4

theorem isOpen_eqLocus (inj : IsLocallyInjective f) (he : f ∘ g₁ = f ∘ g₂) : IsOpen {a | g₁ a = g₂ a} :=
  let g : A → f.Pullback f := fun a ↦ ⟨⟨g₁ a, g₂ a⟩, congr_fun he a⟩
  (isLocallyInjective_iff_isOpen_diagonal.mp inj).preimage (by fun_prop : Continuous g)

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