def definition def or abbrev

`RSPossible`

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

formal statement (Lean)

  58def RSPossible (x : ℝ) : Prop := 0 < x

Definition body.

  59
  60/-- **RSActual**: x is actual iff it is RSNecessary (i.e., x = 1). -/

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

impossible_is_non_positive in IndisputableMonolith.Philosophy.ModalOntologyStructure decl_use
modal_distance_nonneg in IndisputableMonolith.Philosophy.ModalOntologyStructure decl_use
modal_distance_zero_iff_actual in IndisputableMonolith.Philosophy.ModalOntologyStructure decl_use
ph013_modal_certificate in IndisputableMonolith.Philosophy.ModalOntologyStructure decl_use
possibility_is_not_singleton in IndisputableMonolith.Philosophy.ModalOntologyStructure decl_use
possibility_is_positive_ratio in IndisputableMonolith.Philosophy.ModalOntologyStructure decl_use
possible_has_finite_cost in IndisputableMonolith.Philosophy.ModalOntologyStructure decl_use
possible_not_impossible in IndisputableMonolith.Philosophy.ModalOntologyStructure decl_use
RSNecessary in IndisputableMonolith.Philosophy.ModalOntologyStructure decl_use
s5_actuality_implies_possibility in IndisputableMonolith.Philosophy.ModalOntologyStructure decl_use
s5_possible_accessible_to_necessary in IndisputableMonolith.Philosophy.ModalOntologyStructure decl_use

Lean names referenced from this declaration's body.

is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
RSActual in IndisputableMonolith.Philosophy.ModalOntologyStructure decl_use
RSNecessary in IndisputableMonolith.Philosophy.ModalOntologyStructure decl_use