我想归属定义reducible。我很确定我的语法正确,因为我从tutorial (p. 118)逐字拷贝了它。 definition pr1 [reducible] (A : Type) (a b : A) : A := a
attribute pr1 [reducible]
两个属性的组合都不通过语法检查:直接连接到它的定义使得type expected at reducible,而独立声
我想用精益做一些拓扑工作。 作为一个好的开始,我想证明一些关于sets in lean的简单引理。 例如 def inter_to_union (H : a ∈ set.inter A B) : a ∈ set.union A B :=
sorry
或 def set_deMorgan : a ∈ set.inter A B → a ∈ set.compl (set.union (s
给定集合包含的证明及其相反,我希望能够证明两个集合是平等的。 例如,我知道如何证明following statement,并its converse: open set
universe u
variable elem_type : Type u
variable A : set elem_type
variable B : set elem_type
def set_deMorga
精益带有约含排序及其与平等有用的引理,如decidable_linear_order类型类: lemma eq_or_lt_of_not_lt [decidable_linear_order α] {a b : α} (h : ¬ a < b) : a = b ∨ b < a 在这些排序的等式是在=方面都表示: inductive eq {α : Sort u} (a : α) : α → Pro
我试图从chapter 7 of "theorem proving in lean"了解归纳类型。 我给自己设定了证明自然数的是继任者的任务,拥有平等的一个替代性质: inductive natural : Type
| zero : natural
| succ : natural -> natural
lemma succ_over_equality (a b : natural) (