eq_top_iff' — Mathlib

English

Let A be a nonunital subring of R. Then A = ⊤ if and only if every element x of R lies in A.

Русский

Пусть A — неединичное подкольцо кольца R. Тогда A = ⊤ тогда и только если для каждого x ∈ R выполняется x ∈ A.

LaTeX

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

Lean4

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

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