coeff_of_le_one — Mathlib

English

If b ≤ 1, then the entire coefficient function equals a single entry at o with value 0: coeff(b,o) = single 0 o.

Русский

Если b ≤ 1, то коэффициентная функция равна единственному элементу на o со значением 0: coeff(b,o) = single 0 o.

LaTeX

$$$$ \\forall b,o:\\; b \\le 1 \\rightarrow \\operatorname{coeff}(b,o) = \\operatorname{single}(0)\\, o $$$$

Lean4

theorem coeff_of_le_one {b : Ordinal} (hb : b ≤ 1) (o : Ordinal) : coeff b o = single 0 o :=
  by
  ext a
  obtain rfl | ho := eq_or_ne o 0
  · simp
  · obtain rfl | ha := eq_or_ne a 0
    · apply coeff_of_mem_CNF
      rw [CNF.of_le_one hb ho]
      simp
    · rw [single_eq_of_ne ha]
      apply coeff_of_not_mem_CNF
      rw [CNF.of_le_one hb ho]
      simpa using ha

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