18.2. The four quantifier forms
Quantification over the whole real line may be universal or existential. The body can combine equalities, inequalities, conjunctions, disjunctions, negations, and implications:
/-- A universal sentence over the real line. -/
example : ∀ x : ℝ, x ^ 2 ≤ 1 → x ^ 4 - x ^ 2 ≤ 0 := ⊢ ∀ (x : ℝ), x ^ 2 ≤ 1 → x ^ 4 - x ^ 2 ≤ 0
All goals completed! 🐙
/-- An existential sentence over the real line. -/
example : ∃ x : ℝ, x ^ 3 - x - 1 = 0 ∧ 1 < x ∧ x < 2 := ⊢ ∃ x, x ^ 3 - x - 1 = 0 ∧ 1 < x ∧ x < 2
All goals completed! 🐙
The bounded forms use Set.Ioc a b, which denotes (a, b]. The lower
endpoint is excluded and the upper endpoint is included:
/-- Universal quantification over `(0, 1]`. -/
example : ∀ x : ℝ, x ∈ Set.Ioc (0 : ℝ) 1 → x > 0 := ⊢ ∀ x ∈ Set.Ioc 0 1, x > 0
All goals completed! 🐙
/-- Existential quantification over `(0, 1]`.
The upper endpoint is a witness. -/
example : ∃ x : ℝ, x ∈ Set.Ioc (0 : ℝ) 1 ∧ x = 1 := ⊢ ∃ x ∈ Set.Ioc 0 1, x = 1
All goals completed! 🐙
An interval is empty when a ≥ b. Universal statements on an empty
interval are true, while existential statements are false. These examples
also show that the lower endpoint is not part of a nonempty interval:
example : ∀ x : ℝ, x ∈ Set.Ioc (1 : ℝ) 1 → x ^ 2 < 0 := ⊢ ∀ x ∈ Set.Ioc 1 1, x ^ 2 < 0
All goals completed! 🐙
example : ¬ ∃ x : ℝ, x ∈ Set.Ioc (1 : ℝ) 1 ∧ x = x := ⊢ ¬∃ x ∈ Set.Ioc 1 1, x = x
x:ℝhx:x ∈ Set.Ioc 1 1right✝:x = x⊢ False
All goals completed! 🐙
example : ∀ x : ℝ, x ∈ Set.Ioc (0 : ℝ) 1 → x ≠ 0 := ⊢ ∀ x ∈ Set.Ioc 0 1, x ≠ 0
All goals completed! 🐙