Drop placeholders prior to Mathlib4 port.

finite-set-exercises
Joshua Potter 2023-07-26 13:41:55 -06:00
parent 526a11a3f6
commit c3b579aed1
6 changed files with 2 additions and 79 deletions

View File

@ -1,4 +1,3 @@
import Common.Finset
import Common.List import Common.List
import Common.Logic import Common.Logic
import Common.Real import Common.Real

View File

@ -1,17 +0,0 @@
import Mathlib.Data.Finset.Basic
/-! # Common.Finset
Additional theorems and definitions useful in the context of `Finset`s.
-/
namespace Finset
/--
An alternative `Finset.range` function that returns `Fin` indices instead of ``
indices.
-/
def finRange (n : ) : Finset (Fin n) :=
⟨sorry, sorry⟩
end Finset

View File

@ -1,4 +1,3 @@
import Common.Finset
import Common.Geometry.Rectangle.Orthogonal import Common.Geometry.Rectangle.Orthogonal
import Common.List.Basic import Common.List.Basic
import Common.List.NonEmpty import Common.List.NonEmpty
@ -73,19 +72,7 @@ namespace StepFunction
/-- /--
The ordinate set of the `StepFunction`. The ordinate set of the `StepFunction`.
-/ -/
def toSet (sf : StepFunction) : Set Point := def toSet (sf : StepFunction) : Set Point := sorry
i ∈ Finset.finRange sf.ivls.length,
let I := sf.ivls[i]
Rectangle.Orthogonal.toSet
{
tl := ⟨I.left, sf.toFun i⟩,
bl := ⟨I.left, 0⟩,
br := ⟨I.right, 0⟩,
has_right_angle := sorry
},
by simp
end StepFunction end StepFunction

View File

@ -1,4 +1,2 @@
import Common.Real.Floor import Common.Real.Floor
import Common.Real.Rational
import Common.Real.Sequence import Common.Real.Sequence
import Common.Real.Trigonometry

View File

@ -1,18 +0,0 @@
import Mathlib.Data.Real.Basic
/-! # Common.Real.Rational
Additional theorems and definitions useful in the context of rational numbers.
Most of these will likely be deleted once the corresponding functions in
`Mathlib` are ported to Lean 4.
-/
/--
Assert that a real number is irrational.
-/
def irrational (x : ) := x ∉ Set.range RatCast.ratCast
/--
Assert that a real number is rational.
-/
def rational (x : ) := ¬ irrational x

View File

@ -1,26 +0,0 @@
import Mathlib.Data.Real.Basic
/-! # Common.Real.Trigonometry
Additional theorems and definitions useful in the context of trigonometry. Most
of these will likely be deleted once the corresponding functions in `Mathlib`
are ported to Lean 4.
-/
namespace Real
/--
The standard `π` variable with value `3.14159...`.
-/
axiom pi :
/--
The undirected angle at `p₂` between the line segments to `p₁` and `p₃`. If
either of those points equals `p₂`, this is `π / 2`.
-/
axiom angle (p₁ p₂ p₃ : × ) :
noncomputable def euclideanAngle (p₁ p₂ p₃ : × ) :=
if p₁ = p₂ p₂ = p₃ then pi / 2 else angle p₁ p₂ p₃
end Real