Relations lifted to optional values.

Copyright (c) The Iris-Lean Contributors.

def Option.Forall₂ {α : Type u_1} {β : Type u_2} (R : α → β → Prop) : Option α → Option β → Prop

Lift a relation to optional values, relating absence only to absence.

Equations

• Option.Forall₂ R none none = True
• Option.Forall₂ R (some a) (some b) = R a b
• Option.Forall₂ R x✝¹ x✝ = False

theorem Option.Forall₂.getD {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {a : α} {b : β} (hab : R a b) {o : Option α} {o' : Option β} : Forall₂ R o o' → R (o.getD a) (o'.getD b)

theorem Option.Forall₂.equivalence {α : Type u_1} {R : α → α → Prop} (H : Equivalence R) : Equivalence (Forall₂ R)