dite_dite_distrib_left
theorem dite_dite_distrib_left :
∀ {α : Sort u_1} {p q : Prop} [inst : Decidable p] [inst_1 : Decidable q] {a : p → α} {b : ¬p → q → α}
{c : ¬p → ¬q → α},
(dite p a fun hp => dite q (b hp) (c hp)) =
if hq : q then dite p a fun hp => b hp hq else dite p a fun hp => c hp hq
This theorem, named `dite_dite_distrib_left`, states that for any propositions `p` and `q`, and any functions `a`, `b`, `c` of types `p → α`, `¬p → q → α`, and `¬p → ¬q → α` respectively, the expression `(dite p a fun hp => dite q (b hp) (c hp))` is equivalent to the expression `if hq : q then dite p a fun hp => b hp hq else dite p a fun hp => c hp hq`. Here, `dite` is a dependent if-then-else construct in Lean, `p` and `q` are propositions, and `α` is some sort expression. This theorem essentially says that under certain conditions, the nesting order of two dependent if-then-else constructs can be swapped.
More concisely: For any propositions p and q and functions a, b, and c, the dependent if-then-elses `dite p a fun hp => dite q (b hp) (c hp)` and `if hq : q then dite p a fun hp => b hp hq else dite p a fun hp => c hp hq` are equivalent.
|
Eq.heq
theorem Eq.heq : ∀ {α : Sort u_1} {a b : α}, a = b → HEq a b
This theorem, referred to as `Eq.heq`, states that for any type `α` and any two elements `a` and `b` of this type, if `a` equals `b` then `a` and `b` are heterogeneously equal (`HEq`). In other words, it provides an alias for the reverse direction of the `heq_iff_eq` theorem, which establishes the bi-directional relationship between equality (`=`) and heterogeneous equality (`HEq`).
More concisely: For any type `α` and elements `a` and `b` of type `α`, if `a` equals `b`, then `a` and `b` are heterogeneously equal. (`Eq.heq : ∀ (α : Type*) (a b : α), a = b → a HEq b`)
|
HEq.eq
theorem HEq.eq : ∀ {α : Sort u_1} {a b : α}, HEq a b → a = b
This theorem, named `HEq.eq`, states that for any type, denoted by α, and any two objects, a and b, of this type, if a is heterogeneously equal (HEq) to b, then a is also equal (eq) to b. This theorem is an alias (or another way of referring to) the forward direction of the `heq_iff_eq` theorem. In other words, it shows that heterogeneous equality implies the standard equality in Lean's type theory.
More concisely: For any type α and objects a, b of α, if a =^ a' (heterogeneous equality) then a = b (standard equality).
|
dite_dite_distrib_right
theorem dite_dite_distrib_right :
∀ {α : Sort u_1} {p q : Prop} [inst : Decidable p] [inst_1 : Decidable q] {a : p → q → α} {b : p → ¬q → α}
{c : ¬p → α},
dite p (fun hp => dite q (a hp) (b hp)) c =
if hq : q then dite p (fun hp => a hp hq) c else dite p (fun hp => b hp hq) c
This theorem states that for any type `α`, propositions `p` and `q`, a function `a` from proofs of `p` and `q` to `α`, a function `b` from proofs of `p` and negation of `q` to `α`, and a function `c` from disproofs of `p` to `α`, the function that returns `a` if `p` and `q` are true, `b` if `p` is true and `q` is false, and `c` if `p` is false, is equivalent to the function that first checks `q`: if `q` is true, it behaves like `a` if `p` is true and `c` otherwise, and if `q` is false, it behaves like `b` if `p` is true and `c` otherwise. This theorem basically states that the order of checking the propositions `p` and `q` does not affect the result.
More concisely: Given functions `a` from proofs of `p` and `q`, `b` from proofs of `p` and negation of `q`, `c` from disproofs of `p`, and a type `α`, the functions `a if p and q else b if p and q neg else c if not p` and `if q then a if p else b if p else c` are equivalent.
|