参考定理库
本模块提供主展示页面所引用的基础结果。定理元数据会跨模块保存在环境中，
当另一个 #theorem 使用这些结果时，Proof-Script 会自动把它们加入参考文献暂存区。
ProofText
= 参考定理库 <library>
本模块提供主展示页面所引用的基础结果。定理元数据会跨模块保存在环境中，
当另一个 `#theorem` 使用这些结果时，Proof-Script 会自动把它们加入参考文献暂存区。
合取左投影
h.left
/Users/zhoukexin/Mitar/demo/MitarDemo/Library.lean
7 行
#theorem @[theorem_info (
name := "合取左投影",
label := "and-left",
tags := "logic, projection",
note := "从合取命题中取得左侧结论"
)] andLeft (P Q : Prop) (h : P ∧ Q) : P := script
cause "h.left"
□
合取左投影
h.left
/Users/zhoukexin/Mitar/demo/MitarDemo/Library.lean
7 lines
#theorem @[theorem_info (
name := "合取左投影",
label := "and-left",
tags := "logic, projection",
note := "从合取命题中取得左侧结论"
)] andLeft (P Q : Prop) (h : P ∧ Q) : P := script
cause "h.left"
□
上面的证明展示了一个最小但完整的 theorem component。主页面会引用 and-left，并在参考文献板块中链接回本页。
ProofText
上面的证明展示了一个最小但完整的 theorem component。主页面会引用
@thm:and-left，并在参考文献板块中链接回本页。