| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/Launchbury/ (Sammlung formaler Beweise Version 2026-5©) Datei vom 31.4.2026 mit Größe 300 B |
|
Quelle Pointwise.thySprache: Isabelle |
|||||||||||||||
|
theory Pointwise imports Main begin text ‹ a relation to a function. › definition pointwise where "pointwise P m m' = (∀ x. P (m x) (m' x))" lemma pointwiseI[intro]: "(∧ x. P (m x) (m' x)) ==> pointwise P m m'" unfolding poin end
¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet am 2026-06-10) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-06-09