eq_top_iff' — Mathlib

English

A subsemiring A equals the top if and only if every element x of the ambient ring lies in A.

Русский

Подполусемиринг A равен верхнему элементу тогда и только тогда, когда любой элемент кольца принадлежит A.

LaTeX

$$$ A = \top \;\iff\; \forall x, x \in A $$$

Lean4

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

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