setOfTop_eq_univ — Mathlib

English

For a nontrivial codomain R, the set of points where all maps vanish is all of X, i.e., setOfIdeal(top) = univ.

Русский

Для непустого R множество точек, на которых все отображения исчезают, совпадает с X; setOfIdeal(top) = univ.

LaTeX

$$$ setOfIdeal(\\top:C(X,R)) = X \\text{ (i.e. } Set.univ) $$$

Lean4

@[simp]
theorem setOfTop_eq_univ [Nontrivial R] : setOfIdeal (⊤ : Ideal C(X, R)) = Set.univ :=
  Set.univ_subset_iff.mp fun _ _ => mem_setOfIdeal.mpr ⟨1, Submodule.mem_top, one_ne_zero⟩

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