booleans #
This file proves various trivial lemmas about booleans and their relation to decidable propositions.
Notations #
This file introduces the notation !b
for bnot b
, the boolean "not".
Tags #
bool, boolean, De Morgan
@[protected, instance]
If p b
is decidable for all b : bool
, then ∀ b, p b
is decidable
Equations
- bool.decidable_forall_bool = decidable_of_decidable_of_iff and.decidable bool.decidable_forall_bool._proof_1
@[protected, instance]
If p b
is decidable for all b : bool
, then ∃ b, p b
is decidable
Equations
- bool.decidable_exists_bool = decidable_of_decidable_of_iff or.decidable bool.decidable_exists_bool._proof_1
De Morgan's laws for booleans #
@[protected, instance]
Equations
- bool.linear_order = {le := λ (a b : bool), a = ff ∨ b = tt, lt := partial_order.lt._default (λ (a b : bool), a = ff ∨ b = tt), le_refl := bool.linear_order._proof_1, le_trans := bool.linear_order._proof_2, lt_iff_le_not_le := bool.linear_order._proof_3, le_antisymm := bool.linear_order._proof_4, le_total := bool.linear_order._proof_5, decidable_le := infer_instance (λ (a b : bool), or.decidable), decidable_eq := infer_instance (λ (a b : bool), bool.decidable_eq a b), decidable_lt := infer_instance (λ (a b : bool), decidable_lt_of_decidable_le a b)}