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

stzMathClaimSet

12 méthodes propres · 1 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 ; 5 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 stzMathClaimSet("a tampered lesson"). 7 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

Lesson

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

exemple composé

o1 = new stzMathClaimSet("a tampered lesson")
? o1.Lesson()
#--> a tampered lesson

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

aucune extension

Add

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

Claims

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

Count

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

exemple composé

o1 = new stzMathClaimSet("a tampered lesson")
? o1.Count()
#--> 0

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

aucune extension

ToLean

one .lean file: Mathlib, the lesson, every theorem; names made unique by position

exemple composé

o1 = new stzMathClaimSet("a tampered lesson")
? o1.ToLean()
#--> -- a tampered lesson: 0 claim(s) emitted by stzMathClaimSet (plane stzlib-math, M6)
#--> -- check with: lake env lean <this file>   inside a Lake project holding Mathlib
#--> import Mathlib

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

aucune extension

WriteLean

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

Diagnostics

the floor over every claim, in the house rule shape: a false claim is an erroraucune extension

Report

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

IsSound

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

exemple composé

o1 = new stzMathClaimSet("a tampered lesson")
? o1.IsSound()
#--> 1

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

aucune extension

CheckWithLean

through the door, once for the whole fileaucune extension

Why

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

exemple composé

o1 = new stzMathClaimSet("a tampered lesson")
? o1.Why()
#--> the claims of 'a tampered lesson': 0 statement(s), 0 false on the numeric floor; the Lean door is open

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

aucune extension