of_le_one — Mathlib

English

If b ≤ 1, then CNF(b, o) is a simple form: either CNF.zero_left or CNF.one_left depending on o and nonzeroness of o.

Русский

Если b ≤ 1, то CNF(b, o) принимает простую форму: либо CNF.zero_left, либо CNF.one_left в зависимости от o и ненулевости o.

LaTeX

$$$\forall b\,\forall o\; (b \le 1) \Rightarrow CNF(b, o) = [(0, o)] \text{ или } CNF(b, o) = \text{CNF.one_left ho}$$$

Lean4

protected theorem of_le_one {b o : Ordinal} (hb : b ≤ 1) (ho : o ≠ 0) : CNF b o = [(0, o)] :=
  by
  rcases le_one_iff.1 hb with (rfl | rfl)
  exacts [CNF.zero_left ho, CNF.one_left ho]

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