`Vantage`

definition

show as: view math explainer →

module: IndisputableMonolith.RRF.Core.Vantage
domain: RRF
line: 27 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.RRF.Core.Vantage on GitHub at line 27.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  24- `act`: The dynamic perspective (recognition, process, becoming)
  25- `outside`: The objective perspective (physics, measurement, observation)
  26-/
  27inductive Vantage : Type where
  28  | inside : Vantage
  29  | act : Vantage
  30  | outside : Vantage
  31  deriving DecidableEq, Repr, Inhabited
  32
  33namespace Vantage
  34
  35/-- Vantage is finite with exactly 3 elements. -/
  36instance : Fintype Vantage where
  37  elems := ⟨[inside, act, outside], by decide⟩
  38  complete := fun v => by cases v <;> decide
  39
  40/-- The number of vantages. -/
  41theorem card_vantage : Fintype.card Vantage = 3 := rfl
  42
  43/-- Every vantage has a complement pair. -/
  44def complements (v : Vantage) : Vantage × Vantage :=
  45  match v with
  46  | inside  => (act, outside)
  47  | act     => (inside, outside)
  48  | outside => (inside, act)
  49
  50/-- Cyclic successor (for the 3-phase rhythm). -/
  51def succ (v : Vantage) : Vantage :=
  52  match v with
  53  | inside  => act
  54  | act     => outside
  55  | outside => inside
  56
  57/-- Cyclic predecessor. -/

papers checked against this theorem

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