Bool.apply_apply_apply
theorem Bool.apply_apply_apply : ∀ (f : Bool → Bool) (x : Bool), f (f (f x)) = f x
This is a theorem known as Kaminski's Equation. It states that for any function `f` from Boolean values to Boolean values and for any Boolean value `x`, applying the function `f` three times to `x` will give the same result as applying the function `f` once to `x`. In mathematical notation, this can be written as `f(f(f(x))) = f(x)`.
More concisely: For any Boolean function `f`, `f(f(f(x))) = f(x)` holds for all Boolean values `x`.
|
Bool.forall_bool
theorem Bool.forall_bool : ∀ {p : Bool → Prop}, (∀ (b : Bool), p b) ↔ p false ∧ p true
This theorem states that for any property `p` that can be applied to boolean values (`Bool → Prop`), the property holds for all boolean values if and only if the property holds for both `false` and `true`. The theorem is essentially stating that a universal quantification over all booleans is equivalent to checking the property for the two possible boolean values.
More concisely: For any property `p` of boolean values, `p` is universally true if and only if `p false` and `p true` hold.
|
Mathlib.Data.Bool.Basic._auxLemma.1
theorem Mathlib.Data.Bool.Basic._auxLemma.1 : ∀ {p : Bool → Prop}, (∀ (b : Bool), p b) = (p false ∧ p true)
This theorem states that for any predicate `p` that operates on boolean values, the property that `p` holds for all boolean values (`∀ (b : Bool), p b`) is equivalent to the conjunction of `p` holding for `false` and `p` holding for `true` (`p false ∧ p true`). Essentially, it captures the idea that, because there are only two boolean values, checking a predicate on all booleans is the same as checking it on `false` and `true` individually.
More concisely: For any predicate `p` on boolean values, `∀ (b : Bool), p b` is equivalent to `p false ∧ p true`.
|