def surjective (f : ℝ → ℝ) : Statement

Equations

• (f is surjective) = ∀ (y : ℝ), ∃ (x : ℝ), f x = y

def term_IsSurjective : Lean.TrailingParserDescr

Equations

• term_IsSurjective = Lean.ParserDescr.trailingNode `term_IsSurjective 50 80 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " is ") (Lean.ParserDescr.symbol "surjective"))

def injective (f : ℝ → ℝ) : Statement

Equations

• (f is injective) = ∀ (x y : ℝ), f x = f y ⇒ x = y

def term_IsInjective : Lean.TrailingParserDescr

Equations

• term_IsInjective = Lean.ParserDescr.trailingNode `term_IsInjective 50 80 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " is ") (Lean.ParserDescr.symbol "injective"))

def croissante {α β : Type} [LE α] [LE β] (f : α → β) : Statement

Equations

• (f is non-decreasing) = ∀ (x₁ x₂ : α), x₁ ≤ x₂ ⇒ f x₁ ≤ f x₂

def «term_IsNon-decreasing» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def decroissante {α β : Type} [LE α] [LE β] (f : α → β) : Statement

Equations

• (f is non-increasing) = ∀ (x₁ x₂ : α), x₁ ≤ x₂ ⇒ f x₁ ≥ f x₂

def «term_IsNon-increasing» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def limite_suite (u : ℕ → ℝ) (l : ℝ) : Statement

Equations

• (u tends to l) = ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, |u n - l| ≤ ε

def term_TendsTo_ : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def limite_infinie_suite (u : ℕ → ℝ) : Statement

La suite u tends to +∞.

Equations

• (u tends to +∞) = ∀ (A : ℝ), ∃ (N : ℕ), ∀ n ≥ N, u n ≥ A

def «term_TendsTo+∞» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def est_borne_sup (M : ℝ) (u : ℕ → ℝ) : Statement

Equations

• (M is the supremum of u) = ((∀ (n : ℕ), u n ≤ M) ∧ ∀ ε > 0, ∃ (n₀ : ℕ), u n₀ ≥ M - ε)

def term_IsTheSupremumOf_ : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def est_borne_inf (M : ℝ) (u : ℕ → ℝ) : Statement

Equations

• (M is the infimum of u) = ((∀ (n : ℕ), M ≤ u n) ∧ ∀ ε > 0, ∃ (n₀ : ℕ), u n₀ ≤ M + ε)

def term_IsTheInfimumOf_ : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def bounds_above (A : Set ℝ) (x : ℝ) : Statement

Le réel x est un majorant de l'ensemble de réels A.

Equations

• (x bounds from above A) = ∀ a ∈ A, a ≤ x

def term_BoundsFromAbove_ : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def borne_sup (A : Set ℝ) (x : ℝ) : Statement

Le réel x est une borne supérieure de l'ensemble de réels A.

Equations

• (x is the supremum of A) = (x bounds from above A ∧ ∀ (y : ℝ), y bounds from above A ⇒ x ≤ y)

def term_IsTheSupremumOf__1 : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def minorant (A : Set ℝ) (x : ℝ) : Statement

Le réel x est un minorant de l'ensemble de réels A.

Equations

• (x bounds from below A) = ∀ a ∈ A, x ≤ a

def term_BoundsFromBelow_ : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def borne_inf (A : Set ℝ) (x : ℝ) : Statement

Le réel x est une borne inférieure de l'ensemble de réels A.

Equations

• (x is the infimum of A) = (x bounds from below A ∧ ∀ (y : ℝ), y bounds from below A ⇒ x ≤ y)

def term_IsTheInfimumOf__1 : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

theorem m154.inferieur_ssi {x y : ℝ} : x ≤ y ⇔ 0 ≤ y - x

theorem m154.pos_pos {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) : 0 ≤ x * y

theorem m154.neg_neg {x y : ℝ} (hx : x ≤ 0) (hy : y ≤ 0) : 0 ≤ x * y

theorem m154.inferieur_ssi' {x y : ℝ} : x ≤ y ⇔ x - y ≤ 0

theorem m154.inferieur_diff_pos {x y : ℝ} : x ≤ y ⇒ 0 ≤ y - x

theorem m154.diff_pos_inferieur {x y : ℝ} : 0 ≤ y - x ⇒ x ≤ y

theorem m154.inferieur_diff_neg {x y : ℝ} : x ≤ y ⇒ x - y ≤ 0

theorem m154.diff_neg_inferieur {x y : ℝ} : x - y ≤ 0 ⇒ x ≤ y

theorem m154.carre_pos {a : ℝ} : a > 0 ⇒ a ^ 2 > 0

theorem divise_refl (a : ℕ) : a ∣ a

axiom divise_gcd_ssi {a b c : ℕ} : c ∣ a.gcd b ⇔ c ∣ a ∧ c ∣ b

axiom divise_si_divise_gcd {a b c : ℕ} : c ∣ a.gcd b ⇒ c ∣ a ∧ c ∣ b

axiom divise_si_divise_left {a b c : ℕ} : c ∣ a.gcd b ⇒ c ∣ a

axiom divise_si_divise_right {a b c : ℕ} : c ∣ a.gcd b ⇒ c ∣ b

axiom divise_gcd_si {a b c : ℕ} : c ∣ a ⇒ c ∣ b ⇒ c ∣ a.gcd b

axiom gcd_divise_left {a b : ℕ} : a.gcd b ∣ a

axiom gcd_divise_right {a b : ℕ} : a.gcd b ∣ b

theorem divise_antisym {a b : ℕ} : a ∣ b ⇒ b ∣ a ⇒ a = b

theorem divise_def (a b : ℤ) : a ∣ b ⇔ ∃ (k : ℤ), b = a * k

class HasParity (α : Type) : Type

• isEven : Prédicat sur α
• isOdd : Prédicat sur α

def term_IsEven : Lean.TrailingParserDescr

Equations

• term_IsEven = Lean.ParserDescr.trailingNode `term_IsEven 60 60 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " is ") (Lean.ParserDescr.symbol "even"))

def term_IsOdd : Lean.TrailingParserDescr

Equations

• term_IsOdd = Lean.ParserDescr.trailingNode `term_IsOdd 60 60 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " is ") (Lean.ParserDescr.symbol "odd"))

instance instHasParityInt : HasParity ℤ

Equations

• instHasParityInt = { isEven := fun (n : ℤ) => ∃ (k : ℤ), n = 2 * k, isOdd := fun (n : ℤ) => ∃ (k : ℤ), n = 2 * k + 1 }

instance instHasParityForallReal : HasParity (ℝ → ℝ)

Equations

• instHasParityForallReal = { isEven := fun (f : ℝ → ℝ) => ∀ (x : ℝ), f (-x) = f x, isOdd := fun (f : ℝ → ℝ) => ∀ (x : ℝ), f (-x) = -f x }

theorem pair_ou_impair (n : ℤ) : n is even ∨ n is odd

theorem non_pair_et_impair (n : ℤ) : ¬(n is even ∧ n is odd)

theorem abs_inferieur_ssi {x y : ℝ} : |x| ≤ y ⇔ -y ≤ x ∧ x ≤ y

theorem abs_diff (x y : ℝ) : |x - y| = |y - x|

theorem pos_abs {x : ℝ} : |x| > 0 ⇔ x ≠ 0

theorem non_zero_abs_pos {a : ℝ} : a ≠ 0 ⇒ |a| > 0

def delabMax : Lean.PrettyPrinter.Delaborator.Delab

Equations

• One or more equations did not get rendered due to their size.

def delabMin : Lean.PrettyPrinter.Delaborator.Delab

Equations

• One or more equations did not get rendered due to their size.

theorem superieur_max_ssi {α : Type u_1} [LinearOrder α] (p q r : α) : r ≥ max p q ⇔ r ≥ p ∧ r ≥ q

theorem inferieur_max_gauche {α : Type u_1} [LinearOrder α] (p q : α) : p ≤ max p q

theorem inferieur_max_droite {α : Type u_1} [LinearOrder α] (p q : α) : q ≤ max p q

theorem egal_si_abs_diff_neg {a b : ℝ} : |a - b| ≤ 0 ⇒ a = b

theorem egal_si_abs_eps (x y : ℝ) : (∀ ε > 0, |x - y| ≤ ε) ⇒ x = y

theorem abs_plus (x y : ℝ) : |x + y| ≤ |x| + |y|

theorem ineg_triangle (x y z : ℝ) : |x - y| ≤ |x - z| + |z - y|

theorem ineg_triangle' (x y z : ℝ) : |x - y| ≤ |x - z| + |y - z|

theorem ineg_triangle'' (x y z : ℝ) : |x - y| ≤ |z - x| + |z - y|

theorem m154.unicite_limite {u : ℕ → ℝ} {l l' : ℝ} : (u tends to l) ⇒ (u tends to l') ⇒ l = l'

theorem M154.inferieur_mul_droite {a b c : ℝ} (hc : 0 ≤ c) (hab : a ≤ b) : a * c ≤ b * c

theorem M154.inferieur_mul_gauche {a b c : ℝ} (hc : 0 ≤ c) (hab : a ≤ b) : c * a ≤ c * b

theorem M154.inferieur_add_gauche {a b c : ℝ} : a ≤ b ⇒ c + a ≤ c + b

theorem M154.inferieur_add_droite {a b c : ℝ} : a ≤ b ⇒ a + c ≤ b + c

theorem M154.inferieur_simpl_gauche {a b c : ℝ} : c + a ≤ c + b ⇒ a ≤ b

theorem M154.inferieur_simpl_droite {a b c : ℝ} : a + c ≤ b + c ⇒ a ≤ b

def extraction (φ : ℕ → ℕ) : Statement

Equations

• (φ is an extraction) = ∀ (n m : ℕ), n < m ⇒ φ n < φ m

def term_IsAnExtraction : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def suite_cauchy (u : ℕ → ℝ) : Statement

Equations

• (u is Cauchy) = ∀ ε > 0, ∃ (N : ℕ), ∀ p ≥ N, ∀ q ≥ N, |u p - u q| ≤ ε

def term_IsCauchy : Lean.TrailingParserDescr

Equations

• term_IsCauchy = Lean.ParserDescr.trailingNode `term_IsCauchy 50 80 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " is ") (Lean.ParserDescr.symbol "Cauchy"))

def valeur_adherence (u : ℕ → ℝ) (a : ℝ) : Statement

Un réel a est valeur d'adhérence d'une suite u s'il existe une suite extraite de u qui tends to a.

Equations

• (u is a cluster point of a) = ∃ (φ : ℕ → ℕ), φ is an extraction ∧ u ∘ φ tends to a

def term_IsAClusterPointOf_ : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def valAdhDelab : Lean.PrettyPrinter.Delaborator.Delab

Equations

• One or more equations did not get rendered due to their size.

theorem extraction_superieur_id {φ : ℕ → ℕ} : φ is an extraction ⇒ ∀ (n : ℕ), n ≤ φ n

Toute extraction est supérieure à l'identité.

theorem extraction_machine (ψ : ℕ → ℕ) (hψ : ∀ (n : ℕ), ψ n ≥ n) : ∃ (f : ℕ → ℕ), ψ ∘ f is an extraction ∧ ∀ (n : ℕ), f n ≥ n

def tacticVerifie : Lean.ParserDescr

Equations

• tacticVerifie = Lean.ParserDescr.node `tacticVerifie 1024 (Lean.ParserDescr.nonReservedSymbol "verifie" false)

def Verbose.English.Subset {α : Type u_2} (s₁ s₂ : Set α) : Statement

Equations

• Verbose.English.Subset s₁ s₂ = ∀ a ∈ s₁, a ∈ s₂

@[instance 10000]

instance Verbose.English.hasSubset {α : Type u_2} : HasSubset (Set α)

Equations

• Verbose.English.hasSubset = { Subset := Verbose.English.Subset }

theorem le_le_of_abs_le' {α : Type u_2} [LinearOrder α] [AddCommGroup α] [IsOrderedAddMonoid α] {a b : α} : |a| ≤ b ⇒ a ≤ b ∧ -b ≤ a

theorem le_of_abs_le' {α : Type u_2} [LinearOrder α] [AddCommGroup α] [IsOrderedAddMonoid α] {a b : α} : |a| ≤ b ⇒ -b ≤ a

theorem le_antisymm' {α : Type u_2} [PartialOrder α] {a b : α} (h : b ≤ a) (h' : a ≤ b) : a = b

theorem ex_mul_of_dvd {R : Type u_2} [CommSemiring R] {a b : R} (h : a ∣ b) : ∃ (k : R), b = k * a

theorem ex_mul_of_dvd' {a b : ℤ} (h : ∃ (k : ℤ), b = k * a) : a ∣ b

def commandSetup_env : Lean.ParserDescr

Equations

• commandSetup_env = Lean.ParserDescr.node `commandSetup_env 1024 (Lean.ParserDescr.symbol "setup_env")

def «termFct_↦_» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def «termSuite_↦_» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def delabLamWithTypes (domainTy bodyTy : Lean.Expr) (mk : Lean.Ident → Lean.Term → Lean.PrettyPrinter.Delaborator.DelabM Lean.Term) : Lean.PrettyPrinter.Delaborator.Delab

Equations

• One or more equations did not get rendered due to their size.

def delabFct : Lean.PrettyPrinter.Delaborator.Delab

Equations

• One or more equations did not get rendered due to their size.

def delabSuite : Lean.PrettyPrinter.Delaborator.Delab

Equations

• One or more equations did not get rendered due to their size.

def termPrédicatSur_ : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def termStatement : Lean.ParserDescr

Equations

• termStatement = Lean.ParserDescr.node `termStatement 1024 (Lean.ParserDescr.symbol "Statement")