La bibliothèque se documente elle-même · Numérique et optimisation

stzMathClaim

20 méthodes propres · 0 formes avec extensions, rangées sous leur méthode

la source: base/math/stzMathClaim.ring(s'ouvre dans un nouvel onglet) · Toutes les classes · La référence du domaine : Numérique et optimisation

Sous chaque méthode, ses extensions (Q CS XT Z ZZ IB W U) : en gras et cochée, elle existe ; barrée, elle n'existe pas. Les extensions et leur sens

Exemples : 0 viennent des tests de la bibliothèque ; 15 ont été composés à partir de la signature de chaque méthode et exécutés pour cette page, sur un objet neuf, par exemple o1 = new stzMathClaim("3^2 + 4^2 + 1 = 5^2"). 5 méthodes n'en ont pas encore. Exemples exécutés le 2026-10-03 12:54 dans la bibliothèque au commit 0e72e2e2c.

Méthode

Explication, telle que la source la porte

init

(sans commentaire dans la source : le nom se lit comme une phrase) initaucune extension

Kind

(sans commentaire dans la source : le nom se lit comme une phrase) kind

exemple composé

o1 = new stzMathClaim("3^2 + 4^2 + 1 = 5^2")
? o1.Kind()
#--> identity

composé à partir de la signature, exécuté pour cette page

aucune extension

Relation

(sans commentaire dans la source : le nom se lit comme une phrase) relation

exemple composé

o1 = new stzMathClaim("3^2 + 4^2 + 1 = 5^2")
? o1.Relation()
#--> =

composé à partir de la signature, exécuté pour cette page

aucune extension

Lhs

(sans commentaire dans la source : le nom se lit comme une phrase) lhs

exemple composé

o1 = new stzMathClaim("3^2 + 4^2 + 1 = 5^2")
? o1.Lhs()
#--> 3^2 + 4^2 + 1

composé à partir de la signature, exécuté pour cette page

aucune extension

Rhs

(sans commentaire dans la source : le nom se lit comme une phrase) rhs

exemple composé

o1 = new stzMathClaim("3^2 + 4^2 + 1 = 5^2")
? o1.Rhs()
#--> 5^2

composé à partir de la signature, exécuté pour cette page

aucune extension

Over

(sans commentaire dans la source : le nom se lit comme une phrase) over

exemple composé

o1 = new stzMathClaim("3^2 + 4^2 + 1 = 5^2")
? o1.Over()
#--> real

composé à partir de la signature, exécuté pour cette page

aucune extension

Vars

(sans commentaire dans la source : le nom se lit comme une phrase) varsaucune extension

Label

(sans commentaire dans la source : le nom se lit comme une phrase) label

exemple composé

o1 = new stzMathClaim("3^2 + 4^2 + 1 = 5^2")
? o1.Label()
#--> 3^2 + 4^2 + 1 = 5^2

composé à partir de la signature, exécuté pour cette page

aucune extension

Tactic

(sans commentaire dans la source : le nom se lit comme une phrase) tacticaucune extension

Statement

(sans commentaire dans la source : le nom se lit comme une phrase) statement

exemple composé

o1 = new stzMathClaim("3^2 + 4^2 + 1 = 5^2")
? o1.Statement()
#--> 3^2 + 4^2 + 1 = 5^2

composé à partir de la signature, exécuté pour cette page

aucune extension

SamplePoints

the points the floor samples: one for a closed statement, sixteen per variable otherwise, integers where the domain is integers

exemple composé

o1 = new stzMathClaim("3^2 + 4^2 + 1 = 5^2")
? @@( o1.SamplePoints() )
#--> [ [ 0 ] ]

composé à partir de la signature, exécuté pour cette page

aucune extension

Check

the floor's verdict: every sampled point, the first counterexample kept

exemple composé

o1 = new stzMathClaim("3^2 + 4^2 + 1 = 5^2")
? @@( o1.Check() )
#--> [ [ "verdict", 0 ], [ "route", "numeric floor" ], [ "points", 1 ], [ "evidence", "the sides are 26 and 25" ], [ "counterexample", [ 0 ] ] ]

composé à partir de la signature, exécuté pour cette page

aucune extension

IsTrue

(sans commentaire dans la source : le nom se lit comme une phrase) is true

exemple composé

o1 = new stzMathClaim("3^2 + 4^2 + 1 = 5^2")
? o1.IsTrue()
#--> 0

composé à partir de la signature, exécuté pour cette page

aucune extension

LastCheck

(sans commentaire dans la source : le nom se lit comme une phrase) last checkaucune extension

TheoremName

THE DOOR: the Lean statement, and the verdict when Lean is present

exemple composé

o1 = new stzMathClaim("3^2 + 4^2 + 1 = 5^2")
? o1.TheoremName()
#--> claim_3_2_4_2_1_5_2

composé à partir de la signature, exécuté pour cette page

aucune extension

LeanTactic

the tactic: the author's, or the one the kind and the variables call for

exemple composé

o1 = new stzMathClaim("3^2 + 4^2 + 1 = 5^2")
? o1.LeanTactic()
#--> norm_num

composé à partir de la signature, exécuté pour cette page

aucune extension

LeanStatement

(sans commentaire dans la source : le nom se lit comme une phrase) lean statement

exemple composé

o1 = new stzMathClaim("3^2 + 4^2 + 1 = 5^2")
? o1.LeanStatement()
#--> ((3^2 + 4^2 + 1 : ℝ) = 5^2)

composé à partir de la signature, exécuté pour cette page

aucune extension

ToLean

(sans commentaire dans la source : le nom se lit comme une phrase) to lean

exemple composé

o1 = new stzMathClaim("3^2 + 4^2 + 1 = 5^2")
? o1.ToLean()
#--> theorem claim_3_2_4_2_1_5_2 : ((3^2 + 4^2 + 1 : ℝ) = 5^2) := by norm_num

composé à partir de la signature, exécuté pour cette page

aucune extension

CheckWithLean

through the door: a proof when Lean is here, the door's name when it is not; the floor's verdict rides along either wayaucune extension

Why

(sans commentaire dans la source : le nom se lit comme une phrase) why

exemple composé

o1 = new stzMathClaim("3^2 + 4^2 + 1 = 5^2")
? o1.Why()
#--> an identity over the reals, '3^2 + 4^2 + 1 = 5^2': FALSE on the floor, the sides are 26 and 25; the Lean door is open (lean at C:\Lean\elan\bin/lean.exe, project at C:\Lean\stz_lean)

composé à partir de la signature, exécuté pour cette page

aucune extension