eq_top_iff'

Mathlib.Algebra.Ring.Subring.Basic

URI: https://scilib.ai/kg/mathlib#Subring.eq_top_iff'

English

For a subring A of R, A = ⊤ if and only if every element of R lies in A.

Русский

Для подкольца A кольца R верно: A = ⊤ тогда и только тогда, когда каждый элемент R принадлежит A.

LaTeX

$$$A = \\top \\iff \\forall x: R, x \\in A$$$

Lean4

theorem eq_top_iff' (A : Subring R) : A = ⊤ ↔ ∀ x : R, x ∈ A :=
  eq_top_iff.trans ⟨fun h m => h <| mem_top m, fun h m _ => h m⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru