mk_le_mk — Mathlib

English

For NonUnitalSubrings S,S' generated from S,S' as NonUnitalSubsemirings with witnesses h,h', we have (⟨S,h⟩ ≤ ⟨S',h'⟩) iff S ≤ S'.

Русский

Для подполья S,S' и соответствующих структур подпорожденных S,S' верна эквивалентность: ⟨S,h⟩ ≤ ⟨S',h'⟩ тогда и только тогда, когда S ≤ S'.

LaTeX

$$$(⟨S,h⟩ : NonUnitalSubring R) \le (⟨S',h'⟩ : NonUnitalSubring R) \Leftrightarrow S \le S'$$$

Lean4

@[simp]
theorem mk_le_mk {S S' : NonUnitalSubsemiring R} (h h') :
    (⟨S, h⟩ : NonUnitalSubring R) ≤ (⟨S', h'⟩ : NonUnitalSubring R) ↔ S ≤ S' :=
  Iff.rfl

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