theorem
proved
trivialModel_consistent
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.RRF.Models.Trivial on GitHub at line 80.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
77 ⟨(), trivial_balanced⟩
78
79/-- The trivial model is consistent (nonempty at universe 0). -/
80theorem trivialModel_consistent : Nonempty (Octave.{0, 0, 0}) := ⟨trivialOctave⟩
81
82/-! ## Vantage Triple in Trivial Model -/
83
84/-- A unified vantage triple in the trivial model. -/
85def trivialVantageTriple : VantageTriple TrivialState :=
86 VantageTriple.unified ()
87
88theorem trivialVantageTriple_unified : VantageTriple.isUnified trivialVantageTriple :=
89 VantageTriple.unified_is_unified ()
90
91end RRF.Models
92end IndisputableMonolith