one_sub_mem — Mathlib

English

If R is a ring with appropriate order properties and is an integral domain, Ioo(0,1) forms a CancelMonoid.

Русский

Если R кольцо с допустимыми порядковыми свойствами и является областью без делителей нуля, Ioo(0,1) образует CancelMonoid.

LaTeX

$$$\text{CancelMonoid} (\text{Ioo}(0,1).\text{Elem})$$$

Lean4

theorem one_sub_mem {t : β} (ht : t ∈ Ioo (0 : β) 1) : 1 - t ∈ Ioo (0 : β) 1 := by
  simp_all only [mem_Ioo, sub_pos, sub_lt_self_iff, and_self]

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