mathlib documentation

lean_problem_sheets / 2020.relations.random_reln_transitive2

inductive X :

Type

A : X
B : X
C : X

def R (x y : X) :

Prop

Equations

R x y = (x = X.A ∧ y = X.B ∨ x = X.A ∧ y = X.C)

theorem R_fst {x y : X} :

R x y → x = X.A