def definition def or abbrev

`le`

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

formal statement (Lean)

 325def le (n m : LogicNat) : Prop := ∃ k : LogicNat, n + k = m

proof body

Definition body.

 326
 327/-- Strict order on `LogicNat`. -/

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

interp in IndisputableMonolith.Action.PathSpace decl_use
abs_heatFactor_le_one in IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D decl_use
Real in IndisputableMonolith.Compat.Mathlib decl_use
kappa_einstein_eq in IndisputableMonolith.Constants decl_use
hubble_resolution_converges in IndisputableMonolith.Cosmology.HubbleResolution decl_use
phi_power_matches_eta in IndisputableMonolith.Cosmology.MatterAntimatter decl_use
jcost_energy_min_at_ground in IndisputableMonolith.Engineering.EnergyStorageDensityStructure decl_use
jcost_energy_nonneg in IndisputableMonolith.Engineering.EnergyStorageDensityStructure decl_use
strict_transmutation_progress in IndisputableMonolith.Engineering.FissionTransmutationStructure decl_use
cooper_pair_binding_exceeds_thermal in IndisputableMonolith.Engineering.RoomTempSuperconductivityStructure decl_use
prefer_trans in IndisputableMonolith.Ethics.CostModel decl_use
le_antisymm in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
lt in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
total_defect_lower_bound in IndisputableMonolith.Foundation.VariationalDynamics decl_use
D_growth_ge_a in IndisputableMonolith.Gravity.ILGGrowthFactor decl_use
C_kernel_eq_two_minus_phi in IndisputableMonolith.Gravity.ILGSpatialKernel decl_use
epsilon_le_half in IndisputableMonolith.Gravity.JCostInflaton decl_use
r_ref_exact_gt_r in IndisputableMonolith.Gravity.RunningG decl_use
kernel_perturbation_bounded_above in IndisputableMonolith.ILG.Kernel decl_use
kernel_perturbation_ge_one in IndisputableMonolith.ILG.Kernel decl_use
octagon_approximates_pi in IndisputableMonolith.Mathematics.Pi decl_use
prob₁_nonneg in IndisputableMonolith.Measurement.BornRule decl_use
prob₂_nonneg in IndisputableMonolith.Measurement.BornRule decl_use
one_step_factor_le_one in IndisputableMonolith.NavierStokes.DiscreteMaximumPrinciple decl_use
corePairStretchFactor_pos in IndisputableMonolith.NavierStokes.DiscreteNSOperator decl_use
rm2Closed_of_coerciveL2Bound in IndisputableMonolith.NavierStokes.RM2U.RM2Closure decl_use
ancientDecay_implies_A2_integrable in IndisputableMonolith.NavierStokes.RM2U.TailFluxInstantiation decl_use
ancientDecay_implies_tailFlux_vanish in IndisputableMonolith.NavierStokes.RM2U.TailFluxInstantiation decl_use
operatorPairing_of_decayFull in IndisputableMonolith.NavierStokes.RM2U.TailFluxInstantiation decl_use
rescaleLength_tendsto_zero in IndisputableMonolith.NavierStokes.RunningMaxNormalization decl_use

… and 10 more

depends on (1)

Lean names referenced from this declaration's body.

LogicNat in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use