`constZero`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.NonTrivialityFromDistinguishability
domain: Foundation
line: 185 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.NonTrivialityFromDistinguishability on GitHub at line 185.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 182comparison is operative." -/
 183
 184/-- The constant-zero comparison operator. -/
 185def constZero : ComparisonOperator := fun _ _ => 0
 186
 187/-- Constant zero satisfies identity. -/
 188theorem constZero_identity : Identity constZero := by
 189  intro x _; rfl
 190
 191/-- Constant zero satisfies non-contradiction. -/
 192theorem constZero_nonContradiction : NonContradiction constZero := by
 193  intro x y _ _; rfl
 194
 195/-- Constant zero is continuous on the positive quadrant. -/
 196theorem constZero_continuous : ExcludedMiddle constZero := by
 197  unfold ExcludedMiddle
 198  exact continuousOn_const
 199
 200/-- Constant zero is scale-invariant. -/
 201theorem constZero_scaleInvariant : ScaleInvariant constZero := by
 202  intro _ _ _ _ _ _; rfl
 203
 204/-- Constant zero fails distinguishability. -/
 205theorem constZero_not_distinguishable : ¬ Distinguishability constZero := by
 206  intro ⟨_, _, _, _, h⟩
 207  exact h rfl
 208
 209/-- Constant zero fails non-triviality. -/
 210theorem constZero_not_nonTrivial : ¬ NonTrivial constZero := by
 211  intro ⟨_, _, h⟩
 212  exact h rfl
 213
 214/-! ## Summary
 215

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.