I agree Our site saves small pieces of text information (cookies) on your device in order to deliver better content and for statistical purposes. You can disable the usage of cookies by changing the settings of your browser. By browsing our website without changing the browser settings you grant us permission to store that information on your device.
theory Defs imports Main begin fun sum where "sum 0 = 0" | "sum (Suc n) = Suc n + sum n" end
theory Submission imports Defs begin lemma goal1: "n \<le> m \<Longrightarrow> sum n \<le> sum m" sorry lemma goal2: "n <= sum n" sorry lemma goal3: "\<And>M. (\<exists>N. \<forall>n\<ge>N. sum n \<ge> M)" sorry end
theory Check imports Submission begin lemma "n \<le> m \<Longrightarrow> sum n \<le> sum m" by(rule Submission.goal1) lemma "n <= sum n" by(rule Submission.goal2) lemma "\<And>M. (\<exists>N. \<forall>n\<ge>N. sum n \<ge> M)" by(rule Submission.goal3) end
-- Lean version: 3.4.2 -- Mathlib version: 2019-07-31 namespace my def sum : ℕ → ℕ | 0 := 0 | (n + 1) := (n + 1) + sum n end my
import .defs lemma goal1 : ∀ (n m : ℕ), n ≤ m ↔ my.sum n ≤ my.sum m := sorry lemma goal2 : ∀ (n : ℕ), n ≤ my.sum n := sorry lemma goal3 : ∀ (M : ℕ), ∃ (N : ℕ), ∀ (n ≥ N), my.sum n ≥ M := sorry
import .defs .submission lemma lemma1 : ∀ (n m : ℕ), n ≤ m ↔ my.sum n ≤ my.sum m := goal1 lemma lemma2 : ∀ (n : ℕ), n ≤ my.sum n := goal2 lemma lemma3 : ∀ (M : ℕ), ∃ (N : ℕ), ∀ (n ≥ N), my.sum n ≥ M := goal3
theory Defs imports Main begin fun sum where "sum 0 = 0" | "sum (Suc n) = Suc n + sum n" end
theory Submission imports Defs begin lemma goal1: "n \<le> m \<Longrightarrow> sum n \<le> sum m" sorry lemma goal2: "n <= sum n" sorry lemma goal3: "\<And>M. (\<exists>N. \<forall>n\<ge>N. sum n \<ge> M)" sorry end
theory Check imports Submission begin lemma "n \<le> m \<Longrightarrow> sum n \<le> sum m" by(rule Submission.goal1) lemma "n <= sum n" by(rule Submission.goal2) lemma "\<And>M. (\<exists>N. \<forall>n\<ge>N. sum n \<ge> M)" by(rule Submission.goal3) end
-- Lean version: 3.16.2 -- Mathlib version: eb5b7fb7f406385cd1f2efaa15d9c0923541b955 namespace my def sum : ℕ → ℕ | 0 := 0 | (n + 1) := (n + 1) + sum n end my
import .defs lemma goal1 : ∀ (n m : ℕ), n ≤ m ↔ my.sum n ≤ my.sum m := sorry lemma goal2 : ∀ (n : ℕ), n ≤ my.sum n := sorry lemma goal3 : ∀ (M : ℕ), ∃ (N : ℕ), ∀ (n ≥ N), my.sum n ≥ M := sorry
import .defs .submission lemma lemma1 : ∀ (n m : ℕ), n ≤ m ↔ my.sum n ≤ my.sum m := goal1 lemma lemma2 : ∀ (n : ℕ), n ≤ my.sum n := goal2 lemma lemma3 : ∀ (M : ℕ), ∃ (N : ℕ), ∀ (n ≥ N), my.sum n ≥ M := goal3