English
LiftRelO extends a relation R on elements and a relation C on weak sequences to a relation on Option (α × WSeq α) and Option (β × WSeq β), defined by: none—none is true; some(a,s) and some(b,t) require R a b and C s t; otherwise false.
Русский
LiftRelO расширяет отношение R на элементы и отношение C на слабые последовательности до отношения на Option (α × WSeq α) и Option (β × WSeq β): neither—true; some(a,s) и some(b,t) требуют R a b и C s t; иначе — False.
LaTeX
$$$$ \text{LiftRelO}(R,C):\, \mathrm{Option}(\alpha\times\mathrm{WSeq}\alpha) \to \mathrm{Option}(\beta\times\mathrm{WSeq}\beta) \to \mathrm{Prop}, \\ |\text{none},\text{none} \to \text{True}, \\ |\text{some}(a,s),\text{some}(b,t) \to R\,a\,b \land C\,s\,t, \\ |_,_\to \text{False}. $$$$
Lean4
/-- lift a relation to a relation over weak sequences -/
@[simp]
def LiftRelO (R : α → β → Prop) (C : WSeq α → WSeq β → Prop) : Option (α × WSeq α) → Option (β × WSeq β) → Prop
| none, none => True
| some (a, s), some (b, t) => R a b ∧ C s t
| _, _ => False
