精益帶有約含排序及其與平等有用的引理，如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) (
我想歸屬定義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