pith. machine review for the scientific record. sign in
theorem proved term proof

moral_ordering_trans

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 112theorem moral_ordering_trans (a b c : EthicalAction)
 113    (hab : MorallyBetter a b) (hbc : MorallyBetter b c) :
 114    MorallyBetter a c :=

proof body

Term-mode proof.

 115  le_trans hab hbc
 116
 117/-- **Theorem (Better Actions Exist)**: For any non-ideal action, a better one exists.
 118    This is the formal statement that moral improvement is always possible
 119    until the ideal is reached. -/

depends on (12)

Lean names referenced from this declaration's body.