`constZero_identity`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.NonTrivialityFromDistinguishability on GitHub at line 188.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 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
 216Move 1 closure: distinguishability is an Aristotelian content, the
 217algebraic `NonTrivial` predicate is one of its consequences under
 218scale invariance, and the only operator that satisfies all the other

papers checked against this theorem

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