lnot_bit — Mathlib

English

The negation of bit b n distributes over the bit: lnot (bit b n) = bit (not b) (lnot n).

Русский

Логическое отрицание не распределяется над битом: lnot (bit b n) = bit (not b) (lnot n).

LaTeX

$$$$ \operatorname{lnot\_{bit}}(b) : \forall n, \operatorname{lnot}(\operatorname{bit}(b,n)) = \operatorname{bit}(\lnot b)(\operatorname{lnot} n). $$$$

Lean4

@[simp]
theorem lnot_bit (b) : ∀ n, lnot (bit b n) = bit (not b) (lnot n)
  | (n : ℕ) => by simp [lnot]
  | -[n+1] => by simp [lnot]

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