closure_singleton_natCast — Mathlib

English

For every natural number n, closure({n.cast}) = bottom; the subsemiring generated by a natCast is trivial.

Русский

Для каждого натурального числа n замыкание множества {n.cast} равно нижнему элементу; генерируемое natCast подполе тривиально.

LaTeX

$$$\forall n \in \mathbb{N},\; \mathrm{closure} (\{n\}_{R}) = \bot$$$

Lean4

@[simp]
theorem closure_singleton_natCast (n : ℕ) : closure {(n : R)} = ⊥ :=
  bot_unique <| closure_le.2 <| Set.singleton_subset_iff.mpr <| natCast_mem _ _

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