eq_of_forall_π_app_eq — Mathlib

English

If two elements a and b of C have identical π_app values for every Finset J, then a = b.

Русский

Если две точки a и b из C имеют одинаковые значения π_app для каждого Finset J, то a = b.

LaTeX

$$$\\forall (a,b)\\in C, (\\forall J, π_{app}C(·∈J)a = π_{app}C(·∈J)b) \\Rightarrow a=b$$$

Lean4

theorem eq_of_forall_π_app_eq (a b : C) (h : ∀ (J : Finset ι), π_app C (· ∈ J) a = π_app C (· ∈ J) b) : a = b :=
  by
  ext i
  specialize h ({ i } : Finset ι)
  rw [Subtype.ext_iff] at h
  simp only [π_app, ContinuousMap.precomp, ContinuousMap.coe_mk, Set.MapsTo.val_restrict_apply] at h
  exact congr_fun h ⟨i, Finset.mem_singleton.mpr rfl⟩

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