structure RatRect.Rect : Type

• pos : PointR
• size : PointR

structure RatRect.Tiling : Type

• rs : Finset Rect

def RatRect.Rect.width (r : Rect) : ℝ

Equations

• r.width = r.size.x

def RatRect.Rect.height (r : Rect) : ℝ

Equations

• r.height = r.size.y

def RatRect.Rect.x₁ (r : Rect) : ℝ

Equations

• r.x₁ = r.pos.x

def RatRect.Rect.y₁ (r : Rect) : ℝ

Equations

• r.y₁ = r.pos.y

def RatRect.Rect.x₂ (r : Rect) : ℝ

Equations

• r.x₂ = r.x₁ + r.width

def RatRect.Rect.y₂ (r : Rect) : ℝ

Equations

• r.y₂ = r.y₁ + r.height

class RatRect.Rect.WF (r : Rect) : Prop

• width_pos : 0 < r.width
• height_pos : 0 < r.height

def RatRect.Rect.surface (r : Rect) : Set PointR

Equations

• r.surface = Point.ofProd '' Set.Icc r.x₁ r.x₂ ×ˢ Set.Icc r.y₁ r.y₂

def RatRect.Rect.interior (r : Rect) : Set PointR

Equations

• r.interior = Point.ofProd '' Set.Ioo r.x₁ r.x₂ ×ˢ Set.Ioo r.y₁ r.y₂

def RatRect.Rect.boundary (r : Rect) : Set PointR

Equations

• r.boundary = r.surface \ r.interior

def RatRect.Rect.tiledBy (r : Rect) (t : Tiling) : Prop

Equations

• r.tiledBy t = (⋃ r' ∈ t.rs, r'.surface = r.surface)

class RatRect.Tiling.WF (t : Tiling) : Prop

• r_wf (r : Rect) : r ∈ t.rs → r.WF
• rect_eq_of_mem_interior (r₁ : Rect) : r₁ ∈ t.rs → ∀ r₂ ∈ t.rs, ∀ p ∈ r₁.interior, p ∈ r₂.interior → r₁ = r₂
• exi_rect : ∃ (r : Rect), r.WF ∧ r.tiledBy t

def RatRect.Rect.trivTiling (r : Rect) : Tiling

Equations

• r.trivTiling = { rs := {r} }

def RatRect.Rect.rat (r : Rect) : Prop

Equations

• r.rat = (¬Irrational r.width ∨ ¬Irrational r.height)

def RatRect.Tiling.rat (t : Tiling) : Prop

Equations

• t.rat = ∀ r ∈ t.rs, r.rat

theorem RatRect.Rect.wf_def {r : Rect} : r.WF ↔ 0 < r.width ∧ 0 < r.height

@[simp]

theorem RatRect.x₁_lt_x₂ {r : Rect} [wf : r.WF] : r.x₁ < r.x₂

@[simp]

theorem RatRect.y₁_lt_y₂ {r : Rect} [wf : r.WF] : r.y₁ < r.y₂

@[simp]

theorem RatRect.pos_x_eq_x₁ {r : Rect} : r.pos.x = r.x₁

@[simp]

theorem RatRect.pos_y_eq_y₁ {r : Rect} : r.pos.y = r.y₁

@[simp]

theorem RatRect.x₁_le_x₂ {r : Rect} [wf : r.WF] : r.x₁ ≤ r.x₂

@[simp]

theorem RatRect.y₁_le_y₂ {r : Rect} [wf : r.WF] : r.y₁ ≤ r.y₂

@[simp]

theorem RatRect.x₁_ne_x₂ {r : Rect} [wf : r.WF] : r.x₁ ≠ r.x₂

@[simp]

theorem RatRect.y₁_ne_y₂ {r : Rect} [wf : r.WF] : r.y₁ ≠ r.y₂

@[simp]

theorem RatRect.mem_surface {r : Rect} {p : PointR} : p ∈ r.surface ↔ r.x₁ ≤ p.x ∧ p.x ≤ r.x₂ ∧ r.y₁ ≤ p.y ∧ p.y ≤ r.y₂

@[simp]

theorem RatRect.mem_interior {r : Rect} {p : PointR} : p ∈ r.interior ↔ r.x₁ < p.x ∧ p.x < r.x₂ ∧ r.y₁ < p.y ∧ p.y < r.y₂

@[simp]

theorem RatRect.mem_boundary {r : Rect} [wf : r.WF] {p : PointR} : p ∈ r.boundary ↔ (p.x = r.x₁ ∨ p.x = r.x₂) ∧ r.y₁ ≤ p.y ∧ p.y ≤ r.y₂ ∨ (p.y = r.y₁ ∨ p.y = r.y₂) ∧ r.x₁ ≤ p.x ∧ p.x ≤ r.x₂

@[simp]

theorem RatRect.pos_mem_surface {r : Rect} [wf : r.WF] : r.pos ∈ r.surface

@[simp]

theorem RatRect.not_pos_mem_interior {r : Rect} : r.pos ∉ r.interior

@[simp]

theorem RatRect.pos_mem_boundary {r : Rect} [wf : r.WF] : r.pos ∈ r.boundary

@[simp]

theorem RatRect.surface_ne_empty {r : Rect} [wf : r.WF] : r.surface ≠ ∅

@[simp]

theorem RatRect.boundary_ne_empty {r : Rect} [wf : r.WF] : r.boundary ≠ ∅

@[simp]

theorem RatRect.interior_ne_empty {r : Rect} [wf : r.WF] : r.interior ≠ ∅

@[simp]

theorem RatRect.disjoint_interior_boundary {r : Rect} [wf : r.WF] : Disjoint r.interior r.boundary

@[simp]

theorem RatRect.disjoint_boundary_interior {r : Rect} [wf : r.WF] : Disjoint r.boundary r.interior

@[simp]

theorem RatRect.interior_inter_boundary {r : Rect} [wf : r.WF] : r.interior ∩ r.boundary = ∅

@[simp]

theorem RatRect.boundary_inter_interior {r : Rect} [wf : r.WF] : r.boundary ∩ r.interior = ∅

@[simp]

theorem RatRect.interior_union_boundary_eq_surface {r : Rect} [wf : r.WF] : r.interior ∪ r.boundary = r.surface

@[simp]

theorem RatRect.boundary_union_interior_eq_surface {r : Rect} [wf : r.WF] : r.boundary ∪ r.interior = r.surface

@[simp]

theorem RatRect.surface_diff_interior_eq_boundary {r : Rect} : r.surface \ r.interior = r.boundary

@[simp]

theorem RatRect.surface_diff_boundary_eq_interior {r : Rect} [wf : r.WF] : r.surface \ r.boundary = r.interior

instance RatRect.instWFTrivTilingOfWF {r : Rect} [wf : r.WF] : r.trivTiling.WF

@[simp]

theorem RatRect.tiledBy_trivTiling {r : Rect} : r.tiledBy r.trivTiling

@[simp]

theorem RatRect.Tiling.rat_mk {rs : Finset Rect} : { rs := rs }.rat ↔ ∀ r ∈ rs, r.rat

@[simp]

theorem RatRect.trivTiling_rat_iff {r : Rect} : r.trivTiling.rat ↔ r.rat

@[simp]

theorem RatRect.rs_ne_empty {t : Tiling} [wf : t.WF] : t.rs ≠ ∅