Common.Logic.Basic #

Additional theorems and definitions related to basic logic.

theorem not_and_de_morgan {p : Prop} {q : Prop} :

The de Morgan law that distributes negation across a conjunction.

theorem not_or_de_morgan {p : Prop} {q : Prop} :

Renaming of not_or to indicate its relationship to de Morgan's laws.

theorem contraposition {p : Prop} {q : Prop} :

p → q ↔ ¬q → ¬p

The principle of contraposition.

theorem forall_mem_comm {α : Type u_1} {β : Type u_2} {X : Set α} {Y : Set β} (p : α → β → Prop) :

(∀ u ∈ X, ∀ v ∈ Y, p u v) = ∀ v ∈ Y, ∀ u ∈ X, p u v

Universal quantification across nested set memberships can be commuted in either order.