Bool.and_or_inj_right'
theorem Bool.and_or_inj_right' : ∀ {m x y : Bool}, (x && m) = (y && m) ∧ (x || m) = (y || m) ↔ x = y
This theorem, `Bool.and_or_inj_right'`, states that for any three boolean values `m`, `x`, and `y`, the equality of the logical AND and logical OR operations between `x` and `m`, and `y` and `m`, implies that `x` is equal to `y`. In mathematical terms, if (x AND m) equals (y AND m) and (x OR m) equals (y OR m), then x must equal y.
More concisely: If `m` is a boolean value and `(x = (x AND m) = (y AND m) = (y OR m) = (x OR m))`, then `x = y`.
|
Bool.and_or_inj_left'
theorem Bool.and_or_inj_left' : ∀ {m x y : Bool}, (m && x) = (m && y) ∧ (m || x) = (m || y) ↔ x = y
This theorem, named `Bool.and_or_inj_left'`, provides an equivalence in the Boolean logic. It states that for any three Boolean values `m`, `x`, and `y`, the logical 'and' of `m` and `x` being equal to the logical 'and' of `m` and `y`, and the logical 'or' of `m` and `x` being equal to the logical 'or' of `m` and `y`, is equivalent to `x` being equal to `y`. In other words, if `m` interacts with `x` and `y` in the same way both under 'and' and 'or' operations, then `x` and `y` must be the same Boolean value.
More concisely: If for all Boolean values `m`, `x`, and `y`, `(m AND x = m AND y)` and `(m OR x = m OR y)`, then `x = y`.
|
Bool.not_inj'
theorem Bool.not_inj' : ∀ {x y : Bool}, (!x) = !y ↔ x = y
This theorem, known as an alias of `Bool.not_inj_iff`, establishes a key relationship between boolean variables in Lean 4. Essentially, it states that for any two boolean variables `x` and `y`, the negation of `x` equals the negation of `y` if and only if `x` equals `y`.
More concisely: For all boolean variables x and y, x = y if and only if ¬x = ¬y.
|