def
definition
isUnified
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.RRF.Core.Vantage on GitHub at line 97.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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