`get`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

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

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

  83namespace VantageTriple
  84
  85/-- Project a value by vantage. -/
  86def get {α : Type*} (t : VantageTriple α) (v : Vantage) : α :=
  87  match v with
  88  | Vantage.inside  => t.inside
  89  | Vantage.act     => t.act
  90  | Vantage.outside => t.outside
  91
  92/-- A unified triple: all three vantages see the same value. -/
  93def unified {α : Type*} (x : α) : VantageTriple α :=
  94  { inside := x, act := x, outside := x }
  95
  96/-- Predicate: the triple is unified (all equal). -/
  97def isUnified {α : Type*} [DecidableEq α] (t : VantageTriple α) : Prop :=
  98  t.inside = t.act ∧ t.act = t.outside
  99
 100theorem unified_is_unified {α : Type*} [DecidableEq α] (x : α) :
 101    isUnified (unified x) := ⟨rfl, rfl⟩
 102
 103end VantageTriple
 104
 105end RRF.Core
 106end IndisputableMonolith

papers checked against this theorem

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