Bool.decide_iff
theorem Bool.decide_iff : ∀ (p : Prop) [d : Decidable p], decide p = true ↔ p
This theorem, `Bool.decide_iff`, states that for any proposition `p` which is decidable (i.e., either `p` is true or `p` is false, but not both), the function `decide p` returns `true` if and only if `p` is true. Here, `Decidable p` is an instance of the `Decidable` typeclass, meaning that there is a specific function that can decide whether `p` is true or false. The `↔` symbol represents logical equivalence, so `decide p = true ↔ p` means that `decide p` being true is logically equivalent to `p` being true.
More concisely: Thedecidable proposition `p` is logically equivalent to the Boolean value `decide p` being `true`.
|
Bool.bool_iff_false
theorem Bool.bool_iff_false : ∀ {b : Bool}, ¬b = true ↔ b = false
This theorem, `Bool.bool_iff_false`, states that for all boolean variables `b`, the proposition "`b` is not `true`" is equivalent to the proposition "`b` is `false`". This is an inherent property of Boolean logic, where a variable can only hold `true` or `false`, and thus if it is not `true`, it must necessarily be `false`.
More concisely: For all boolean variables b, b is false if and only if it is not true.
|