pith. machine review for the scientific record. sign in
theorem proved term proof

three_point_closure

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

 218theorem three_point_closure
 219    {a b c : ℝ}
 220    (hb : 1 < b)
 221    (h0 : gapAffineLogR a b c 0 = 0)
 222    (h1 : gapAffineLogR a b c 1 = 1)
 223    (hneg1 : gapAffineLogR a b c (-1) = -2) :
 224    ThreePointClosure a b c := by

proof body

Term-mode proof.

 225  have hparams := affine_log_parameters_forced hb h0 h1 hneg1
 226  exact ⟨hparams.1, hparams.2.1, hparams.2.2,
 227         three_point_forces_canonical_gap hb h0 h1 hneg1⟩
 228
 229end
 230end GapFunctionForcing
 231end RSBridge
 232end IndisputableMonolith

depends on (6)

Lean names referenced from this declaration's body.