bit_le — Mathlib

English

For any Bool b and natural m ≤ n, bit b m ≤ bit b n.

Русский

Для любой булевой переменной b и натуральных m ≤ n выполняется bit b m ≤ bit b n.

LaTeX

$$$$ \forall (b : \mathrm{Bool}) \{m,n : \mathbb{N}\}, m \le n \Rightarrow \text{bit}(b,m) \le \text{bit}(b,n). $$$$

Lean4

theorem bit_le : ∀ (b : Bool) {m n : ℕ}, m ≤ n → bit b m ≤ bit b n
  | true, _, _, h => by dsimp [bit]; cutsat
  | false, _, _, h => by dsimp [bit]; cutsat

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