theorem
proved
wrapper
moral_ordering_refl
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)
109theorem moral_ordering_refl (a : EthicalAction) : MorallyBetter a a :=
proof body
One-line wrapper that applies le_refl.
110 le_refl _
111
depends on (3)
Lean names referenced from this declaration's body.
-
le_refl
in IndisputableMonolith.Foundation.ArithmeticFromLogic
decl_use
-
EthicalAction
in IndisputableMonolith.Philosophy.ObjectiveMoralityStructure
decl_use
-
MorallyBetter
in IndisputableMonolith.Philosophy.ObjectiveMoralityStructure
decl_use