noncomputable def ManualEuclideanR2.sqNorm (x : ℝ × ℝ) : ℝ

Equations

• ManualEuclideanR2.sqNorm x = x.1 ^ 2 + x.2 ^ 2

noncomputable def ManualEuclideanR2.sqDist (x y : ℝ × ℝ) : ℝ

Equations

• ManualEuclideanR2.sqDist x y = (x.1 - y.1) ^ 2 + (x.2 - y.2) ^ 2

theorem ManualEuclideanR2.addInverseR (x : ℝ) : x - x = 0

theorem ManualEuclideanR2.sqDistZero (x : ℝ × ℝ) : sqDist x x = 0

theorem ManualEuclideanR2.eucDistIsNormDiff (x y : ℝ × ℝ) : sqDist x y = sqNorm (x - y)

noncomputable def ManualEuclideanR2.euclideanNorm (x : ℝ × ℝ) : ℝ

Equations

• ManualEuclideanR2.euclideanNorm x = √(ManualEuclideanR2.sqNorm x)

noncomputable def ManualEuclideanR2.euclideanDist (x y : ℝ × ℝ) : ℝ

Equations

• ManualEuclideanR2.euclideanDist x y = √(ManualEuclideanR2.sqDist x y)

theorem ManualEuclideanR2.sqDist_nonneg (x y : ℝ × ℝ) : 0 ≤ sqDist x y

theorem ManualEuclideanR2.euclideanDist_nonneg (x y : ℝ × ℝ) : 0 ≤ euclideanDist x y

def ManualEuclideanR2.LimitR2toR (f : ℝ × ℝ → ℝ) (a : ℝ × ℝ) (L : ℝ) : Prop

Equations

• ManualEuclideanR2.LimitR2toR f a L = ∀ ε > 0, ∃ δ > 0, ∀ (x : ℝ × ℝ), 0 < ManualEuclideanR2.euclideanDist x a ∧ ManualEuclideanR2.euclideanDist x a < δ → |f x - L| < ε

def ManualEuclideanR2.LimitR2toR2 (f : ℝ × ℝ → ℝ × ℝ) (a L : ℝ × ℝ) : Prop

Equations

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

def ManualEuclideanR2.LimitRtoR2 (f : ℝ → ℝ × ℝ) (a : ℝ) (L : ℝ × ℝ) : Prop

Equations

• ManualEuclideanR2.LimitRtoR2 f a L = ∀ ε > 0, ∃ δ > 0, ∀ (x : ℝ), 0 < |x - a| ∧ |x - a| < δ → ManualEuclideanR2.euclideanDist (f x) L < ε

def ManualEuclideanR2.ConvergesR2 (seq : ℕ → ℝ × ℝ) (L : ℝ × ℝ) : Prop

Equations

• ManualEuclideanR2.ConvergesR2 seq L = ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, ManualEuclideanR2.euclideanDist L (seq n) < ε

theorem ManualEuclideanR2.sub_sq_eq_sq_sub (x y : ℝ) : (x - y) ^ 2 = (y - x) ^ 2

theorem ManualEuclideanR2.eucDistComm (x y : ℝ × ℝ) : euclideanDist x y = euclideanDist y x

Example Check

def ManualEuclideanR2.proj₁ (p : ℝ × ℝ) : ℝ

Equations

• ManualEuclideanR2.proj₁ p = p.1

def ManualEuclideanR2.pt_a : ℝ × ℝ

Equations

• ManualEuclideanR2.pt_a = (2, 3)

def ManualEuclideanR2.limit_val : ℝ

Equations

• ManualEuclideanR2.limit_val = 2

def ManualEuclideanR2.example_limit_statement : Prop

Equations

• ManualEuclideanR2.example_limit_statement = ManualEuclideanR2.LimitR2toR ManualEuclideanR2.proj₁ ManualEuclideanR2.pt_a ManualEuclideanR2.limit_val

theorem ManualEuclideanR2.sq_order_preserve (a b : ℝ) : 0 ≤ a ∧ 0 ≤ b ∧ a ^ 2 ≤ b ^ 2 → a ≤ b

theorem ManualEuclideanR2.sqNormNonnegR2 (x : ℝ × ℝ) : sqNorm x ≥ 0

theorem ManualEuclideanR2.sqNormEqEucNormSq (x : ℝ × ℝ) : sqNorm x = euclideanNorm x ^ 2

theorem ManualEuclideanR2.sqrtNonneg (a : ℝ) : a ≥ 0 → √a ≥ 0

theorem ManualEuclideanR2.eucNormNonNegR2 (x : ℝ × ℝ) : euclideanNorm x ≥ 0

theorem ManualEuclideanR2.sqBothSidesR2Norm (x y : ℝ × ℝ) : euclideanNorm x ≤ euclideanNorm y ↔ sqNorm x ≤ sqNorm y

theorem ManualEuclideanR2.addSqsNonnegR (a b : ℝ) : 0 ≤ a ^ 2 + b ^ 2

theorem ManualEuclideanR2.sqSqrtEqn (a b c d : ℝ) : (√(a ^ 2 + b ^ 2) + √(c ^ 2 + d ^ 2)) ^ 2 = a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 + 2 * √(a ^ 2 + b ^ 2) * √(c ^ 2 + d ^ 2)

theorem ManualEuclideanR2.algIneq1Rlemma (a b : ℝ) : a ≤ b → 2 * a ≤ 2 * b

theorem ManualEuclideanR2.babyCauchySchwarzR (a b c d : ℝ) : (a * c + b * d) ^ 2 ≤ (a ^ 2 + b ^ 2) * (c ^ 2 + d ^ 2)

theorem ManualEuclideanR2.algIneq1R (a b c d : ℝ) : 2 * a * c + 2 * b * d ≤ 2 * √((a ^ 2 + b ^ 2) * (c ^ 2 + d ^ 2))

theorem ManualEuclideanR2.addIneqBothSidesR (a b c : ℝ) : a ≤ b → c + a ≤ c + b

theorem ManualEuclideanR2.hassoc (x y : ℝ × ℝ) : x.1 ^ 2 + y.1 ^ 2 + 2 * x.1 * y.1 + (x.2 ^ 2 + y.2 ^ 2 + 2 * x.2 * y.2) = x.1 ^ 2 + (y.1 ^ 2 + 2 * x.1 * y.1 + (x.2 ^ 2 + y.2 ^ 2 + 2 * x.2 * y.2))

theorem ManualEuclideanR2.hassoc2 (x y : ℝ × ℝ) : x.1 ^ 2 + x.2 ^ 2 + y.1 ^ 2 + y.2 ^ 2 + 2 * √(x.1 ^ 2 + x.2 ^ 2) * √(y.1 ^ 2 + y.2 ^ 2) = x.1 ^ 2 + (x.2 ^ 2 + y.1 ^ 2 + y.2 ^ 2 + 2 * √(x.1 ^ 2 + x.2 ^ 2) * √(y.1 ^ 2 + y.2 ^ 2))

theorem ManualEuclideanR2.euclideanNormTriangle (x y : ℝ × ℝ) : euclideanNorm (x + y) ≤ euclideanNorm x + euclideanNorm y

theorem ManualEuclideanR2.euclideanDistTriangle (x y z : ℝ × ℝ) : euclideanDist x z ≤ euclideanDist x y + euclideanDist y z

theorem ManualEuclideanR2.abs_fst_sub_fst_le_euclideanDist (x a : ℝ × ℝ) : |x.1 - a.1| ≤ euclideanDist x a

def ManualEuclideanR2.IsOpenR (S : Set ℝ) : Prop

Equations

• ManualEuclideanR2.IsOpenR S = ∀ s ∈ S, ∃ ε > 0, ∀ (x : ℝ), |s - x| < ε → x ∈ S

def ManualEuclideanR2.IsOpenR2 (S : Set (ℝ × ℝ)) : Prop

Equations

• ManualEuclideanR2.IsOpenR2 S = ∀ s ∈ S, ∃ ε > 0, ∀ (x : ℝ × ℝ), ManualEuclideanR2.euclideanDist s x < ε → x ∈ S

def ManualEuclideanR2.IsClosedR2 (S : Set (ℝ × ℝ)) : Prop

Equations

• ManualEuclideanR2.IsClosedR2 S = ManualEuclideanR2.IsOpenR2 Sᶜ

theorem ManualEuclideanR2.checkUniv (S : Set (ℝ × ℝ)) : S = Set.univ → IsOpenR2 S

theorem ManualEuclideanR2.setContra (x : ℝ × ℝ) (s : Set (ℝ × ℝ)) : x ∈ s ∧ x ∈ sᶜ → False

theorem ManualEuclideanR2.le_of_not_ltR (a b : ℝ) : ¬a < b → b ≤ a

def ManualEuclideanR2.IsBoundedR2 (s : Set (ℝ × ℝ)) : Prop

Equations

• ManualEuclideanR2.IsBoundedR2 s = ∃ (C : ℝ), ∀ x ∈ s, ManualEuclideanR2.euclideanNorm x ≤ C

def ManualEuclideanR2.IsOpenCoverR2 {ι : Type u} (U : ι → Set (ℝ × ℝ)) (K : Set (ℝ × ℝ)) : Prop

Equations

• ManualEuclideanR2.IsOpenCoverR2 U K = ((∀ (i : ι), ManualEuclideanR2.IsOpenR2 (U i)) ∧ K ⊆ ⋃ (i : ι), U i)

def ManualEuclideanR2.IsCompactR2Subcover {ι : Type u} (K : Set (ℝ × ℝ)) : Prop

Equations

• ManualEuclideanR2.IsCompactR2Subcover K = ∀ (U : ι → Set (ℝ × ℝ)), ManualEuclideanR2.IsOpenCoverR2 U K → ∃ (s : Finset ι), s.Nonempty ∧ K ⊆ ⋃ i ∈ s, U i

def ManualEuclideanR2.IsCptR2SubcoverCompl {ι : Type u} (K : Set (ℝ × ℝ)) : Prop

Equations

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

theorem ManualEuclideanR2.TypeEqSetInterLemma (ι : Type u) [Nonempty ι] (s : Finset ι) (F : ι → Set (ℝ × ℝ)) : ⋂ i ∈ s, F i = ⋂ (i : ↥s), F ↑i

theorem ManualEuclideanR2.iInterInterCase (ι : Type u) [Nonempty ι] (s : Finset ι) (h : s.Nonempty) (F : ι → Set (ℝ × ℝ)) (K : Set (ℝ × ℝ)) : ⋂ (i : ↥s), F ↑i ∩ K = (⋂ (i : ↥s), F ↑i) ∩ K

theorem ManualEuclideanR2.SetEmptyComplInter (A B : Set (ℝ × ℝ)) : ∅ = Aᶜ ∩ B → B ⊆ A

theorem ManualEuclideanR2.ExistsIntroBcNonempty (ι : Type u) [Nonempty ι] : ∃ (_i : ι), True

theorem ManualEuclideanR2.SetNegLeftProj (A B : Set (ℝ × ℝ)) (x : ℝ × ℝ) : x ∉ A → x ∉ A ∩ B

theorem ManualEuclideanR2.SetNegRightProj (A B : Set (ℝ × ℝ)) (x : ℝ × ℝ) : x ∉ B → x ∉ A ∩ B

theorem ManualEuclideanR2.ComplLemma (ι : Type u) [Nonempty ι] (K : Set (ℝ × ℝ)) (U : ι → Set (ℝ × ℝ)) : K ⊆ ⋃ (i : ι), U i ↔ ∅ = ⋂ (i : ι), (U i)ᶜ ∩ K

theorem ManualEuclideanR2.ComplLemmaFinset (ι : Type u) [Nonempty ι] (s : Finset ι) (K : Set (ℝ × ℝ)) (U : ι → Set (ℝ × ℝ)) : K ⊆ ⋃ i ∈ s, U i ↔ ∅ = (⋂ i ∈ s, (U i)ᶜ) ∩ K

theorem ManualEuclideanR2.eqSubcoverComplDefs (ι : Type u) [Nonempty ι] (K : Set (ℝ × ℝ)) : IsCompactR2Subcover K ↔ IsCptR2SubcoverCompl K

def ManualEuclideanR2.FiniteIntersectionPropertyR2 (ι : Type) (U : ι → Set (ℝ × ℝ)) : Prop

Equations

• ManualEuclideanR2.FiniteIntersectionPropertyR2 ι U = ∀ (s : Finset ι), (⋂ i ∈ s, U i).Nonempty

def ManualEuclideanR2.IsCompactR2Seq (K : Set (ℝ × ℝ)) : Prop

Equations

• ManualEuclideanR2.IsCompactR2Seq K = ∀ (u : ℕ → ℝ × ℝ), (∀ (n : ℕ), u n ∈ K) → ∃ (L : ℝ × ℝ) (φ : ℕ → ℕ), L ∈ K ∧ StrictMono φ ∧ ManualEuclideanR2.ConvergesR2 (u ∘ φ) L

theorem ManualEuclideanR2.exists_seq_of_infinite_mem {x : ℝ × ℝ} {u : ℕ → ℝ × ℝ} (h : ∀ ε > 0, {n : ℕ | euclideanDist (u n) x < ε}.Infinite) : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ConvergesR2 (u ∘ φ) x

theorem ManualEuclideanR2.algIneq2R (a b c : ℝ) : a < b - c → a + c < b

theorem ManualEuclideanR2.EqCptSubcoverSeqDefs (K : Set (ℝ × ℝ)) : (∀ {ι : Type} [Nonempty ι], IsCompactR2Subcover K) ↔ IsCompactR2Seq K

def ManualEuclideanR2.EqCptSubcoverSeqDefs.S (this : DecidableEq (ℝ × ℝ)) (next_pt : Finset (ℝ × ℝ) → ℝ × ℝ) : ℕ → Finset (ℝ × ℝ)

Equations

• ManualEuclideanR2.EqCptSubcoverSeqDefs.S this next_pt 0 = ∅
• ManualEuclideanR2.EqCptSubcoverSeqDefs.S this next_pt n.succ = ManualEuclideanR2.EqCptSubcoverSeqDefs.S this next_pt n ∪ {next_pt (ManualEuclideanR2.EqCptSubcoverSeqDefs.S this next_pt n)}

def ManualEuclideanR2.LimitSubsetsRtoR2' {X : Set ℝ} {Y : Set (ℝ × ℝ)} (f : ↑X → ↑Y) (a : ↑X) (L : ↑Y) : Prop

Equations

• ManualEuclideanR2.LimitSubsetsRtoR2' f a L = ∀ ε > 0, ∃ δ > 0, ∀ (x : ↑X), dist x a < δ ∧ x ≠ a → ManualEuclideanR2.euclideanDist ↑(f x) ↑L < ε

def ManualEuclideanR2.IsCtsRtoR2 {X : Set ℝ} {Y : Set (ℝ × ℝ)} (f : ↑X → ↑Y) : Prop

Equations

• ManualEuclideanR2.IsCtsRtoR2 f = ∀ (x : ↑X), ManualEuclideanR2.LimitSubsetsRtoR2' f x (f x)

def ManualEuclideanR2.UnitInterval : Set ℝ

Equations

• ManualEuclideanR2.UnitInterval = {r : ℝ | 0 ≤ r ∧ r ≤ 1}

def ManualEuclideanR2.IsPathInR2 (S : Set (ℝ × ℝ)) : Prop

Equations

• ManualEuclideanR2.IsPathInR2 S = ∃ (φ : ↑ManualEuclideanR2.UnitInterval → ↑S), Function.Surjective φ ∧ ManualEuclideanR2.IsCtsRtoR2 φ

def ManualEuclideanR2.IsOpenCoverR {ι : Type} (U : ι → Set ℝ) (K : Set ℝ) : Prop

Equations

• ManualEuclideanR2.IsOpenCoverR U K = ((∀ (i : ι), ManualEuclideanR2.IsOpenR (U i)) ∧ K ⊆ ⋃ (i : ι), U i)

def ManualEuclideanR2.IsCompactRSubcover {ι : Type} (K : Set ℝ) : Prop

Equations

• ManualEuclideanR2.IsCompactRSubcover K = ∀ (U : ι → Set ℝ), ManualEuclideanR2.IsOpenCoverR U K → ∃ (s : Finset ι), s.Nonempty ∧ K ⊆ ⋃ i ∈ s, U i

def ManualEuclideanR2.ConvergesR (seq : ℕ → ℝ) (L : ℝ) : Prop

Equations

• ManualEuclideanR2.ConvergesR seq L = ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, |L - seq n| < ε

def ManualEuclideanR2.IsCompactRSeq (K : Set ℝ) : Prop

Equations

• ManualEuclideanR2.IsCompactRSeq K = ∀ (u : ℕ → ℝ), (∀ (n : ℕ), u n ∈ K) → ∃ (L : ℝ) (φ : ℕ → ℕ), L ∈ K ∧ StrictMono φ ∧ ManualEuclideanR2.ConvergesR (u ∘ φ) L

theorem ManualEuclideanR2.absDistTriangleR (x y z : ℝ) : |x - z| ≤ |x - y| + |y - z|

theorem ManualEuclideanR2.setContraR (x : ℝ) (s : Set ℝ) : x ∈ s ∧ x ∈ sᶜ → False

theorem ManualEuclideanR2.SetNegLeftProjR (A B : Set ℝ) (x : ℝ) : x ∉ A → x ∉ A ∩ B

theorem ManualEuclideanR2.SetNegRightProjR (A B : Set ℝ) (x : ℝ) : x ∉ B → x ∉ A ∩ B

theorem ManualEuclideanR2.SetEmptyComplInterR (A B : Set ℝ) : ∅ = Aᶜ ∩ B → B ⊆ A

theorem ManualEuclideanR2.ComplLemmaR {ι' : Type u_1} [Nonempty ι'] (K : Set ℝ) (U : ι' → Set ℝ) : K ⊆ ⋃ (i : ι'), U i ↔ ∅ = ⋂ (i : ι'), (U i)ᶜ ∩ K

theorem ManualEuclideanR2.TypeEqSetInterLemmaR {ι' : Type u_1} (s : Finset ι') (F : ι' → Set ℝ) : ⋂ i ∈ s, F i = ⋂ (i : ↥s), F ↑i

theorem ManualEuclideanR2.iInterInterCaseR {ι' : Type u_1} (s : Finset ι') (h : s.Nonempty) (F : ι' → Set ℝ) (K : Set ℝ) : ⋂ (i : ↥s), F ↑i ∩ K = (⋂ (i : ↥s), F ↑i) ∩ K

theorem ManualEuclideanR2.ComplLemmaFinsetR {ι' : Type u_1} (s : Finset ι') (K : Set ℝ) (U : ι' → Set ℝ) : K ⊆ ⋃ i ∈ s, U i ↔ ∅ = (⋂ i ∈ s, (U i)ᶜ) ∩ K

theorem ManualEuclideanR2.exists_seq_of_infinite_mem_R {x : ℝ} {u : ℕ → ℝ} (h : ∀ ε > 0, {n : ℕ | |u n - x| < ε}.Infinite) : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ConvergesR (u ∘ φ) x

theorem ManualEuclideanR2.EqCptRSubcoverSeqDefs (K : Set ℝ) : (∀ {ι' : Type} [Nonempty ι'], IsCompactRSubcover K) ↔ IsCompactRSeq K

theorem ManualEuclideanR2.CtsImagesCptRtoR2 {ι : Type} [Nonempty ι] {X : Set ℝ} {Y : Set (ℝ × ℝ)} (f : ↑X → ↑Y) (hcts : IsCtsRtoR2 f) (hsurj : Function.Surjective f) (hcpt : IsCompactRSeq X) : IsCompactR2Subcover Y

theorem ManualEuclideanR2.PathsCompact {ι : Type} [Nonempty ι] (S : Set (ℝ × ℝ)) : IsPathInR2 S → IsCompactR2Subcover S