structure Point (α : Type u_2) : Type u_2

• x : α
• y : α

theorem Point.ext_iff {α : Type u_2} {x y : Point α} : x = y ↔ x.x = y.x ∧ x.y = y.y

theorem Point.ext {α : Type u_2} {x y : Point α} : x.x = y.x → x.y = y.y → x = y

@[instance_reducible]

instance instInhabitedPoint {a✝ : Type u_2} [Inhabited a✝] : Inhabited (Point a✝)

Equations

• instInhabitedPoint = { default := instInhabitedPoint.default }

@[instance_reducible]

instance instDecidableEqPoint {α✝ : Type u_2} [DecidableEq α✝] : DecidableEq (Point α✝)

Equations

• instDecidableEqPoint = instDecidableEqPoint.decEq

def instDecidableEqPoint.decEq {α✝ : Type u_2} [DecidableEq α✝] (x✝ x✝¹ : Point α✝) : Decidable (x✝ = x✝¹)

Equations

• instDecidableEqPoint.decEq { x := a, y := a_1 } { x := b, y := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance instFintypePoint {α✝ : Type u_2} [Fintype α✝] : Fintype (Point α✝)

Equations

• instFintypePoint = Fintype.ofEquiv ((_ : α✝) × α✝) (Point.proxyTypeEquiv α✝)

@[reducible, inline]

abbrev PointN : Type

Equations

• PointN = Point ℕ

@[reducible, inline]

abbrev PointZ : Type

Equations

• PointZ = Point ℤ

@[reducible, inline]

abbrev PointR : Type

Equations

• PointR = Point ℝ

def Point.ofProd {α : Type u_1} (p : α × α) : Point α

Equations

• Point.ofProd p = { x := p.1, y := p.2 }

def Point.toProd {α : Type u_1} (p : Point α) : α × α

Equations

• p.toProd = (p.x, p.y)

@[instance_reducible]

instance Point.instRepr {α : Type u_1} [ha : Repr α] : Repr (Point α)

Equations

• Point.instRepr = { reprPrec := fun (a : Point α) => Point.casesOn (motive := fun (x : Point α) => ℕ → Std.Format) a fun (x y : α) (prec : ℕ) => (x, y).repr prec }

@[instance_reducible]

instance Point.instHashable {α : Type u_1} [Hashable α] : Hashable (Point α)

Equations

• Point.instHashable = { hash := fun (p : Point α) => hash p.toProd }

def Point.le {α : Type u_1} [ha : LinearOrder α] (a b : Point α) : Prop

Equations

• a.le b = (a.y < b.y ∨ a.y = b.y ∧ a.x ≤ b.x)

def Point.lt {α : Type u_1} [ha : LinearOrder α] (a b : Point α) : Prop

Equations

• a.lt b = (a.y < b.y ∨ a.y = b.y ∧ a.x < b.x)

@[instance_reducible]

instance Point.instDecidableLe {α : Type u_1} [ha : LinearOrder α] {a b : Point α} : Decidable (a.le b)

Equations

• Point.instDecidableLe = match h : compare a.y b.y with | Ordering.lt => isTrue ⋯ | Ordering.gt => isFalse ⋯ | Ordering.eq => match h₁ : decide (a.x ≤ b.x) with | true => isTrue ⋯ | false => isFalse ⋯

@[instance_reducible]

instance Point.instLinearOrder {α : Type u_1} [ha : LinearOrder α] : LinearOrder (Point α)

Equations

• Point.instLinearOrder = { le := Point.le, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯, min := fun (a b : Point α) => if a.le b then a else b, max := fun (a b : Point α) => if a.le b then b else a, compare := fun (a b : Point α) => compareOfLessAndEq a b, le_total := ⋯, toDecidableLE := fun (a b : Point α) => inferInstance, min_def := ⋯, max_def := ⋯, compare_eq_compareOfLessAndEq := ⋯ }

theorem Point.le_def {α : Type u_1} [ha : LinearOrder α] {a b : Point α} : a ≤ b ↔ a.le b

theorem Point.lt_def {α : Type u_1} [ha : LinearOrder α] {a b : Point α} : a < b ↔ a.lt b

@[simp]

theorem Point.mk_le {α : Type u_1} [ha : LinearOrder α] {x₁ y₁ x₂ y₂ : α} : { x := x₁, y := y₁ } ≤ { x := x₂, y := y₂ } ↔ { x := x₁, y := y₁ }.le { x := x₂, y := y₂ }

@[simp]

theorem Point.mk_lt {α : Type u_1} [ha : LinearOrder α] {x₁ y₁ x₂ y₂ : α} : { x := x₁, y := y₁ } < { x := x₂, y := y₂ } ↔ { x := x₁, y := y₁ }.lt { x := x₂, y := y₂ }

def Point.add {α : Type u_1} [Add α] (a b : Point α) : Point α

Equations

• a.add b = { x := a.x + b.x, y := a.y + b.y }

@[instance_reducible]

instance Point.instAdd {α : Type u_1} [Add α] : Add (Point α)

Equations

• Point.instAdd = { add := Point.add }

theorem Point.add_def {α : Type u_1} [Add α] {a b : Point α} : a + b = { x := a.x + b.x, y := a.y + b.y }

@[simp]

theorem Point.mk_add_mk {α : Type u_1} [Add α] {x₁ y₁ x₂ y₂ : α} : { x := x₁, y := y₁ } + { x := x₂, y := y₂ } = { x := x₁ + x₂, y := y₁ + y₂ }

@[simp]

theorem Point.x_add {α : Type u_1} [ha : Add α] {p₁ p₂ : Point α} : (p₁ + p₂).x = p₁.x + p₂.x

@[simp]

theorem Point.y_add {α : Type u_1} [ha : Add α] {p₁ p₂ : Point α} : (p₁ + p₂).y = p₁.y + p₂.y

def Point.sub {α : Type u_1} [Sub α] (a b : Point α) : Point α

Equations

• a.sub b = { x := a.x - b.x, y := a.y - b.y }

@[instance_reducible]

instance Point.instSub {α : Type u_1} [Sub α] : Sub (Point α)

Equations

• Point.instSub = { sub := Point.sub }

theorem Point.sub_def {α : Type u_1} [Sub α] {a b : Point α} : a - b = { x := a.x - b.x, y := a.y - b.y }

@[simp]

theorem Point.mk_sub_mk {α : Type u_1} [Sub α] {x₁ y₁ x₂ y₂ : α} : { x := x₁, y := y₁ } - { x := x₂, y := y₂ } = { x := x₁ - x₂, y := y₁ - y₂ }

@[simp]

theorem Point.x_sub {α : Type u_1} [ha : Sub α] {p₁ p₂ : Point α} : (p₁ - p₂).x = p₁.x - p₂.x

@[simp]

theorem Point.y_sub {α : Type u_1} [ha : Sub α] {p₁ p₂ : Point α} : (p₁ - p₂).y = p₁.y - p₂.y

def Point.mul {α : Type u_1} [Mul α] (a b : Point α) : Point α

Equations

• a.mul b = { x := a.x * b.x, y := a.y * b.y }

@[instance_reducible]

instance Point.instMul {α : Type u_1} [Mul α] : Mul (Point α)

Equations

• Point.instMul = { mul := Point.mul }

theorem Point.mul_def {α : Type u_1} [Mul α] {a b : Point α} : a * b = { x := a.x * b.x, y := a.y * b.y }

@[simp]

theorem Point.mk_mul_mk {α : Type u_1} [Mul α] {x₁ y₁ x₂ y₂ : α} : { x := x₁, y := y₁ } * { x := x₂, y := y₂ } = { x := x₁ * x₂, y := y₁ * y₂ }

@[simp]

theorem Point.x_mul {α : Type u_1} [ha : Mul α] {p₁ p₂ : Point α} : (p₁ * p₂).x = p₁.x * p₂.x

@[simp]

theorem Point.y_mul {α : Type u_1} [ha : Mul α] {p₁ p₂ : Point α} : (p₁ * p₂).y = p₁.y * p₂.y

def Point.div {α : Type u_1} [Div α] (a b : Point α) : Point α

Equations

• a.div b = { x := a.x / b.x, y := a.y / b.y }

@[instance_reducible]

instance Point.instDiv {α : Type u_1} [Div α] : Div (Point α)

Equations

• Point.instDiv = { div := Point.div }

theorem Point.div_def {α : Type u_1} [Div α] {a b : Point α} : a / b = { x := a.x / b.x, y := a.y / b.y }

@[simp]

theorem Point.mk_div_mk {α : Type u_1} [Div α] {x₁ y₁ x₂ y₂ : α} : { x := x₁, y := y₁ } / { x := x₂, y := y₂ } = { x := x₁ / x₂, y := y₁ / y₂ }

@[simp]

theorem Point.x_div {α : Type u_1} [ha : Div α] {p₁ p₂ : Point α} : (p₁ / p₂).x = p₁.x / p₂.x

@[simp]

theorem Point.y_div {α : Type u_1} [ha : Div α] {p₁ p₂ : Point α} : (p₁ / p₂).y = p₁.y / p₂.y

@[instance_reducible]

instance Point.instZero {α : Type u_1} [ha : Zero α] : Zero (Point α)

Equations

• Point.instZero = { zero := { x := 0, y := 0 } }

theorem Point.zero_def {α : Type u_1} [ha : Zero α] : 0 = { x := 0, y := 0 }

@[instance_reducible]

instance Point.instOne {α : Type u_1} [ha : One α] : One (Point α)

Equations

• Point.instOne = { one := { x := 1, y := 1 } }

theorem Point.one_def {α : Type u_1} [ha : One α] : 1 = { x := 1, y := 1 }

@[instance_reducible]

instance Point.instNatCast {α : Type u_1} [ha : NatCast α] : NatCast (Point α)

Equations

• Point.instNatCast = { natCast := fun (n : ℕ) => { x := ↑n, y := ↑n } }

theorem Point.natCast_def {α : Type u_1} [ha : NatCast α] {n : ℕ} : ↑n = { x := ↑n, y := ↑n }

@[instance_reducible]

instance Point.instIntCast {α : Type u_1} [ha : IntCast α] : IntCast (Point α)

Equations

• Point.instIntCast = { intCast := fun (n : ℤ) => { x := ↑n, y := ↑n } }

theorem Point.intCast_def {α : Type u_1} [ha : IntCast α] {n : ℤ} : ↑n = { x := ↑n, y := ↑n }

@[instance_reducible]

instance Point.instNeg {α : Type u_1} [ha : Neg α] : Neg (Point α)

Equations

• Point.instNeg = { neg := fun (x : Point α) => match x with | { x := x, y := y } => { x := -x, y := -y } }

theorem Point.neg_def {α : Type u_1} [ha : Neg α] {p : Point α} : -p = { x := -p.x, y := -p.y }

@[simp]

theorem Point.neg_mk {α : Type u_1} [ha : Neg α] {x y : α} : -{ x := x, y := y } = { x := -x, y := -y }

@[simp]

theorem Point.x_neg {α : Type u_1} [ha : Neg α] {p : Point α} : (-p).x = -p.x

@[simp]

theorem Point.y_neg {α : Type u_1} [ha : Neg α] {p : Point α} : (-p).y = -p.y

@[instance_reducible]

instance Point.instAddSemigroup {α : Type u_1} [ha : AddSemigroup α] : AddSemigroup (Point α)

Equations

• Point.instAddSemigroup = { toAdd := Point.instAdd, add_assoc := ⋯ }

@[instance_reducible]

instance Point.instAddZeroClass {α : Type u_1} [ha : AddZeroClass α] : AddZeroClass (Point α)

Equations

• Point.instAddZeroClass = { toZero := Point.instZero, toAdd := Point.instAdd, zero_add := ⋯, add_zero := ⋯ }

@[instance_reducible]

instance Point.instAddMonoid {α : Type u_1} [ha : AddMonoid α] : AddMonoid (Point α)

Equations

• Point.instAddMonoid = { toAddSemigroup := Point.instAddSemigroup, toZero := Point.instAddZeroClass.toZero, zero_add := ⋯, add_zero := ⋯, nsmul := fun (c : ℕ) (x : Point α) => match x with | { x := x, y := y } => { x := c • x, y := c • y }, nsmul_zero := ⋯, nsmul_succ := ⋯ }

theorem Point.nsmul_def {α : Type u_1} [ha : AddMonoid α] {c : ℕ} {p : Point α} : c • p = { x := c • p.x, y := c • p.y }

@[simp]

theorem Point.nsmul_mk {α : Type u_1} [ha : AddMonoid α] {c : ℕ} {x y : α} : c • { x := x, y := y } = { x := c • x, y := c • y }

@[instance_reducible]

instance Point.instSubNegMonoid {α : Type u_1} [ha : SubNegMonoid α] : SubNegMonoid (Point α)

Equations

• Point.instSubNegMonoid = { toAddMonoid := Point.instAddMonoid, toNeg := Point.instNeg, toSub := Point.instSub, zsmul := fun (c : ℤ) (x : Point α) => match x with | { x := x, y := y } => { x := c • x, y := c • y }, sub_eq_add_neg := ⋯, zsmul_zero' := ⋯, zsmul_succ' := ⋯, zsmul_neg' := ⋯ }

theorem Point.zsmul_def {α : Type u_1} [ha : SubNegMonoid α] {c : ℤ} {p : Point α} : c • p = { x := c • p.x, y := c • p.y }

@[simp]

theorem Point.zsmul_mk {α : Type u_1} [ha : SubNegMonoid α] {c : ℤ} {x y : α} : c • { x := x, y := y } = { x := c • x, y := c • y }

@[instance_reducible]

instance Point.instAddCommMagma {α : Type u_1} [ha : AddCommMagma α] : AddCommMagma (Point α)

Equations

• Point.instAddCommMagma = { toAdd := Point.instAdd, add_comm := ⋯ }

@[instance_reducible]

instance Point.instDistrib {α : Type u_1} [ha : Distrib α] : Distrib (Point α)

Equations

• Point.instDistrib = { toMul := Point.instMul, toAdd := Point.instAdd, left_distrib := ⋯, right_distrib := ⋯ }

@[instance_reducible]

instance Point.instMulZeroClass {α : Type u_1} [ha : MulZeroClass α] : MulZeroClass (Point α)

Equations

• Point.instMulZeroClass = { toMul := Point.instMul, toZero := Point.instZero, zero_mul := ⋯, mul_zero := ⋯ }

@[instance_reducible]

instance Point.instSemigroup {α : Type u_1} [ha : Semigroup α] : Semigroup (Point α)

Equations

• Point.instSemigroup = { toMul := Point.instMul, mul_assoc := ⋯ }

@[instance_reducible]

instance Point.instMulOneClass {α : Type u_1} [ha : MulOneClass α] : MulOneClass (Point α)

Equations

• Point.instMulOneClass = { toOne := Point.instOne, toMul := Point.instMul, one_mul := ⋯, mul_one := ⋯ }

@[instance_reducible]

instance Point.instAddMonoidWithOne {α : Type u_1} [ha : AddMonoidWithOne α] : AddMonoidWithOne (Point α)

Equations

• Point.instAddMonoidWithOne = { toNatCast := Point.instNatCast, toAddMonoid := Point.instAddMonoid, toOne := Point.instOne, natCast_zero := ⋯, natCast_succ := ⋯ }

@[instance_reducible]

instance Point.instAddGroup {α : Type u_1} [ha : AddGroup α] : AddGroup (Point α)

Equations

• Point.instAddGroup = { toSubNegMonoid := Point.instSubNegMonoid, neg_add_cancel := ⋯ }

@[instance_reducible]

instance Point.instAddGroupWithOne {α : Type u_1} [ha : AddGroupWithOne α] : AddGroupWithOne (Point α)

Equations

• Point.instAddGroupWithOne = { toIntCast := Point.instIntCast, toAddMonoidWithOne := Point.instAddMonoidWithOne, toNeg := Point.instAddGroup.toNeg, toSub := Point.instAddGroup.toSub, toZSMul := Point.instAddGroup.toZSMul, sub_eq_add_neg := ⋯, zsmul_zero' := ⋯, zsmul_succ' := ⋯, zsmul_neg' := ⋯, neg_add_cancel := ⋯, intCast_ofNat := ⋯, intCast_negSucc := ⋯ }

@[instance_reducible]

instance Point.instAddCommSemigroup {α : Type u_1} [ha : AddCommSemigroup α] : AddCommSemigroup (Point α)

Equations

• Point.instAddCommSemigroup = { toAddSemigroup := Point.instAddSemigroup, add_comm := ⋯ }

@[instance_reducible]

instance Point.instAddCommMonoid {α : Type u_1} [ha : AddCommMonoid α] : AddCommMonoid (Point α)

Equations

• Point.instAddCommMonoid = { toAddMonoid := Point.instAddMonoid, add_comm := ⋯ }

@[instance_reducible]

instance Point.instNonUnitalNonAssocSemiring {α : Type u_1} [ha : NonUnitalNonAssocSemiring α] : NonUnitalNonAssocSemiring (Point α)

Equations

• Point.instNonUnitalNonAssocSemiring = { toAddCommMonoid := Point.instAddCommMonoid, toMul := Point.instDistrib.toMul, left_distrib := ⋯, right_distrib := ⋯, zero_mul := ⋯, mul_zero := ⋯ }

@[instance_reducible]

instance Point.instSemigroupWithZero {α : Type u_1} [ha : SemigroupWithZero α] : SemigroupWithZero (Point α)

Equations

• Point.instSemigroupWithZero = { toSemigroup := Point.instSemigroup, toZero := Point.instMulZeroClass.toZero, zero_mul := ⋯, mul_zero := ⋯ }

@[instance_reducible]

instance Point.instNonUnitalSemiring {α : Type u_1} [ha : NonUnitalSemiring α] : NonUnitalSemiring (Point α)

Equations

• Point.instNonUnitalSemiring = { toNonUnitalNonAssocSemiring := Point.instNonUnitalNonAssocSemiring, mul_assoc := ⋯ }

@[instance_reducible]

instance Point.instMulZeroOneClass {α : Type u_1} [ha : MulZeroOneClass α] : MulZeroOneClass (Point α)

Equations

• Point.instMulZeroOneClass = { toMulOneClass := Point.instMulOneClass, toZero := Point.instMulZeroClass.toZero, zero_mul := ⋯, mul_zero := ⋯ }

@[instance_reducible]

instance Point.instAddCommMonoidWithOne {α : Type u_1} [ha : AddCommMonoidWithOne α] : AddCommMonoidWithOne (Point α)

Equations

• Point.instAddCommMonoidWithOne = { toAddMonoidWithOne := Point.instAddMonoidWithOne, add_comm := ⋯ }

@[instance_reducible]

instance Point.instNonAssocSemiring {α : Type u_1} [ha : NonAssocSemiring α] : NonAssocSemiring (Point α)

Equations

• Point.instNonAssocSemiring = { toNonUnitalNonAssocSemiring := Point.instNonUnitalNonAssocSemiring, toOne := Point.instMulZeroOneClass.toOne, one_mul := ⋯, mul_one := ⋯, toNatCast := Point.instAddCommMonoidWithOne.toNatCast, natCast_zero := ⋯, natCast_succ := ⋯ }

@[instance_reducible]

instance Point.instMonoid {α : Type u_1} [ha : Monoid α] : Monoid (Point α)

Equations

• Point.instMonoid = { toSemigroup := Point.instSemigroup, toOne := Point.instMulOneClass.toOne, one_mul := ⋯, mul_one := ⋯, npow := npowRecAuto, npow_zero := ⋯, npow_succ := ⋯ }

@[instance_reducible]

instance Point.instMonoidWithZero {α : Type u_1} [ha : MonoidWithZero α] : MonoidWithZero (Point α)

Equations

• Point.instMonoidWithZero = { toMonoid := Point.instMonoid, toZero := Point.instMulZeroOneClass.toZero, zero_mul := ⋯, mul_zero := ⋯ }

@[instance_reducible]

instance Point.instSemiring {α : Type u_1} [ha : Semiring α] : Semiring (Point α)

Equations

• Point.instSemiring = { toAddCommMonoid := Point.instAddCommMonoid, toMonoid := Point.instMonoidWithZero.toMonoid, zero_mul := ⋯, mul_zero := ⋯, left_distrib := ⋯, right_distrib := ⋯, toNatCast := Point.instNonAssocSemiring.toNatCast, natCast_zero := ⋯, natCast_succ := ⋯ }

@[instance_reducible]

instance Point.instAddCommGroup {α : Type u_1} [ha : AddCommGroup α] : AddCommGroup (Point α)

Equations

• Point.instAddCommGroup = { toAddGroup := Point.instAddGroup, add_comm := ⋯ }

@[instance_reducible]

instance Point.instRing {α : Type u_1} [ha : Ring α] : Ring (Point α)

Equations

• Point.instRing = { toSemiring := Point.instSemiring, toNeg := Point.instAddCommGroup.toNeg, toSub := Point.instAddCommGroup.toSub, toZSMul := Point.instAddCommGroup.toZSMul, sub_eq_add_neg := ⋯, zsmul_zero' := ⋯, zsmul_succ' := ⋯, zsmul_neg' := ⋯, neg_add_cancel := ⋯, toIntCast := Point.instAddGroupWithOne.toIntCast, intCast_ofNat := ⋯, intCast_negSucc := ⋯ }

theorem Point.eq_zero_iff {α : Type u_1} [Zero α] {p : Point α} : p = 0 ↔ p.x = 0 ∧ p.y = 0

theorem Point.zero_eq_iff {α : Type u_1} [Zero α] {p : Point α} : 0 = p ↔ p.x = 0 ∧ p.y = 0

@[simp]

theorem Point.mk_eq_zero_iff {α : Type u_1} [Zero α] {x y : α} : { x := x, y := y } = 0 ↔ x = 0 ∧ y = 0

@[simp]

theorem Point.zero_eq_mk_iff {α : Type u_1} [Zero α] {x y : α} : 0 = { x := x, y := y } ↔ x = 0 ∧ y = 0

instance Point.instAddLeftStrictMono {α : Type u_1} [ha₁ : LinearOrder α] [ha₂ : Ring α] [ha : AddLeftStrictMono α] : AddLeftStrictMono (Point α)

instance Point.instAddRightStrictMono {α : Type u_1} [ha₁ : LinearOrder α] [ha₂ : Ring α] [ha : AddRightStrictMono α] : AddRightStrictMono (Point α)

instance Point.instMulLeftStrictMono {α : Type u_1} [ha₁ : LinearOrder α] [ha₂ : Ring α] [ha : MulLeftStrictMono α] : MulLeftStrictMono (Point α)

instance Point.instMulRightStrictMono {α : Type u_1} [ha₁ : LinearOrder α] [ha₂ : Ring α] [ha : MulRightStrictMono α] : MulRightStrictMono (Point α)

@[instance_reducible]

instance Point.instOfNat {α : Type u_1} {n : ℕ} [ha : OfNat α n] : OfNat (Point α) n

Equations

• Point.instOfNat = { ofNat := { x := OfNat.ofNat n, y := OfNat.ofNat n } }

theorem Point.ofNat_def {α : Type u_1} {n : ℕ} [ha : OfNat α n] : OfNat.ofNat n = { x := OfNat.ofNat n, y := OfNat.ofNat n }

theorem Point.ofNat_ring_def {α : Type u_1} {n : ℕ} [ha : Ring α] : OfNat.ofNat n = { x := ↑n, y := ↑n }

@[simp]

theorem Point.x_ofNat {α : Type u_1} {n : ℕ} [ha : Ring α] : (OfNat.ofNat n).x = ↑n

@[simp]

theorem Point.y_ofNat {α : Type u_1} {n : ℕ} [ha : Ring α] : (OfNat.ofNat n).y = ↑n

@[simp]

theorem Point.add_self_eq_zero_iff {α : Type u_1} [ha₁ : Ring α] [ha₂ : NoZeroDivisors α] [ha₃ : InjectiveOfNat α] {a : Point α} : a + a = 0 ↔ a = 0

def Point.dist {α : Type u_1} [ha₁ : LinearOrder α] [ha₂ : Ring α] (a b : Point α) : α

Equations

• a.dist b = max |a.x - b.x| |a.y - b.y|

@[simp]

theorem Point.mk_dist_mk {α : Type u_1} [ha₁ : LinearOrder α] [ha₂ : Ring α] {x₁ y₁ x₂ y₂ : α} : { x := x₁, y := y₁ }.dist { x := x₂, y := y₂ } = max |x₁ - x₂| |y₁ - y₂|

theorem Point.dist_comm {α : Type u_1} [ha₁ : LinearOrder α] [ha₂ : Ring α] {a b : Point α} : a.dist b = b.dist a

@[simp]

theorem Point.dist_self {α : Type u_1} [ha₁ : LinearOrder α] [ha₂ : Ring α] [ha₃ : IsOrderedAddMonoid α] {a : Point α} : a.dist a = 0

@[simp]

theorem Point.dist_eq_zero_iff {α : Type u_1} [ha₁ : LinearOrder α] [ha₂ : Ring α] [ha₃ : IsOrderedAddMonoid α] {a b : Point α} : a.dist b = 0 ↔ a = b

@[simp]

theorem Point.triangle {α : Type u_1} [ha₁ : LinearOrder α] [ha₂ : Ring α] [ha₃ : IsOrderedAddMonoid α] {a b c : Point α} : a.dist c ≤ a.dist b + b.dist c

theorem Point.dist_le_iff {α : Type u_1} [ha₁ : LinearOrder α] [ha₂ : Ring α] {a b : Point α} {d : α} : a.dist b ≤ d ↔ max |a.x - b.x| |a.y - b.y| ≤ d

@[simp]

theorem Point.dist_le_zero_iff {α : Type u_1} [ha₁ : LinearOrder α] [ha₂ : Ring α] [ha₃ : IsOrderedAddMonoid α] {a b : Point α} : a.dist b ≤ 0 ↔ a = b

@[simp]

theorem Point.zero_le_dist {α : Type u_1} [ha₁ : LinearOrder α] [ha₂ : Ring α] [ha₃ : IsOrderedAddMonoid α] {a b : Point α} : 0 ≤ a.dist b

@[simp]

theorem Point.not_dist_lt_zero {α : Type u_1} [ha₁ : LinearOrder α] [ha₂ : Ring α] [ha₃ : IsOrderedAddMonoid α] {a b : Point α} : ¬a.dist b < 0

@[simp]

theorem Point.dist_add_left_cancel {α : Type u_1} [ha₁ : LinearOrder α] [ha₂ : Ring α] {a b c : Point α} : (c + a).dist (c + b) = a.dist b

@[simp]

theorem Point.dist_add_right_cancel {α : Type u_1} [ha₁ : LinearOrder α] [ha₂ : Ring α] {a b c : Point α} : (a + c).dist (b + c) = a.dist b

@[simp]

theorem Point.dist_add_cancel_left_left {α : Type u_1} [ha₁ : LinearOrder α] [ha₂ : Ring α] {a b c : Point α} : (c + a).dist (c + b) = a.dist b

@[simp]

theorem Point.dist_add_cancel_left_right {α : Type u_1} [ha₁ : LinearOrder α] [ha₂ : Ring α] {a b c : Point α} : (c + a).dist (b + c) = a.dist b

@[simp]

theorem Point.dist_add_cancel_right_left {α : Type u_1} [ha₁ : LinearOrder α] [ha₂ : Ring α] {a b c : Point α} : (a + c).dist (c + b) = a.dist b

@[simp]

theorem Point.dist_add_cancel_right_right {α : Type u_1} [ha₁ : LinearOrder α] [ha₂ : Ring α] {a b c : Point α} : (a + c).dist (b + c) = a.dist b

@[simp]

theorem Point.neg_dist_neg {α : Type u_1} [ha₁ : LinearOrder α] [ha₂ : Ring α] {a b : Point α} : (-a).dist (-b) = a.dist b

@[simp]

theorem Point.dist_sub_cancel_left {α : Type u_1} [ha₁ : LinearOrder α] [ha₂ : Ring α] {a b c : Point α} : (c - a).dist (c - b) = a.dist b

@[simp]

theorem Point.dist_sub_cancel_right {α : Type u_1} [ha₁ : LinearOrder α] [ha₂ : Ring α] {a b c : Point α} : (a - c).dist (b - c) = a.dist b

@[simp]

theorem Point.dist_nonneg {α : Type u_1} [ha₁ : LinearOrder α] [ha₂ : Ring α] [ha₃ : AddLeftMono α] [ha₄ : AddRightMono α] {a b : Point α} : 0 ≤ a.dist b

@[simp]

theorem Point.abs_dist {α : Type u_1} [ha₁ : LinearOrder α] [ha₂ : Ring α] [ha₃ : AddLeftMono α] [ha₄ : AddRightMono α] {a b : Point α} : |a.dist b| = a.dist b

@[simp]

theorem Point.int_dist_lt_one_iff {a b : PointZ} : dist a b < 1 ↔ a = b

@[simp]

theorem Point.int_dist_le_one_iff {a b : PointZ} : dist a b ≤ 1 ↔ a = b ∨ dist a b = 1

def Point.rect {α : Type u_1} [ha₁ : LocallyFiniteOrderList α] (x₁ y₁ x₂ y₂ : α) : List (Point α)

Equations

• Point.rect x₁ y₁ x₂ y₂ = do let y ← List.icc y₁ y₂ let x ← List.icc x₁ x₂ pure { x := x, y := y }

def Point.rectRel {α : Type u_1} [ha₁ : LocallyFiniteOrderList α] [ha₂ : Ring α] (p : Point α) (dx₁ dy₁ dx₂ dy₂ : α) : List (Point α)

Equations

• p.rectRel dx₁ dy₁ dx₂ dy₂ = Point.rect (p.x - dx₁) (p.y - dy₁) (p.x + dx₂) (p.y + dy₂)

def Point.nbhd {α : Type u_1} [ha₁ : LocallyFiniteOrderList α] [ha₂ : Ring α] (a : Point α) (d : α) : List (Point α)

Equations

• a.nbhd d = a.rectRel d d d d

@[simp]

theorem Point.mem_rect {α : Type u_1} [ha₁ : LocallyFiniteOrderList α] {a : Point α} {x₁ x₂ y₁ y₂ : α} : a ∈ rect x₁ y₁ x₂ y₂ ↔ x₁ ≤ a.x ∧ a.x ≤ x₂ ∧ y₁ ≤ a.y ∧ a.y ≤ y₂

@[simp]

theorem Point.mem_rectRel {α : Type u_1} [ha₁ : LocallyFiniteOrderList α] [ha₂ : Ring α] {a b : Point α} {dx₁ dx₂ dy₁ dy₂ : α} : b ∈ a.rectRel dx₁ dy₁ dx₂ dy₂ ↔ a.x - dx₁ ≤ b.x ∧ b.x ≤ a.x + dx₂ ∧ a.y - dy₁ ≤ b.y ∧ b.y ≤ a.y + dy₂

@[simp]

theorem Point.mem_nbhd {α : Type u_1} [ha₁ : LocallyFiniteOrderList α] [ha₂ : Ring α] [ha₃ : IsOrderedAddMonoid α] {a b : Point α} {d : α} : b ∈ a.nbhd d ↔ a.dist b ≤ d

theorem Point.finite_ofPred_dist_le {c : PointZ} {d : ℕ} : {p : PointZ | dist p c ≤ ↑d}.Finite

@[simp]

theorem Point.forall_le_iff_le_xx_iff₁ {α : Type u_1} [ha₁ : LinearOrder α] [ha₂ : Ring α] {a b : α} : (∀ (p : Point α), p.x ≤ a ↔ p.x ≤ b) ↔ a = b

@[simp]

theorem Point.forall_le_iff_le_yy_iff₁ {α : Type u_1} [ha₁ : LinearOrder α] [ha₂ : Ring α] {a b : α} : (∀ (p : Point α), p.y ≤ a ↔ p.y ≤ b) ↔ a = b

@[simp]

theorem Point.forall_le_iff_le_xy_iff₁ {α : Type u_1} [ha₁ : LinearOrder α] [ha₂ : Ring α] [ha₃ : IsOrderedAddMonoid α] [ha₄ : ZeroLEOneClass α] [ha₅ : NeZero 1] {a b : α} : (∀ (p : Point α), p.x ≤ a ↔ p.y ≤ b) ↔ False

@[simp]

theorem Point.forall_le_iff_le_yx_iff₁ {α : Type u_1} [ha₁ : LinearOrder α] [ha₂ : Ring α] [ha₃ : IsOrderedAddMonoid α] [ha₄ : ZeroLEOneClass α] [ha₅ : NeZero 1] {a b : α} : (∀ (p : Point α), p.y ≤ a ↔ p.x ≤ b) ↔ False

@[simp]

theorem Point.forall_le_iff_le_xx_iff₂ {α : Type u_1} [ha₁ : LinearOrder α] [ha₂ : Ring α] [ha₃ : IsOrderedAddMonoid α] [ha₄ : ZeroLEOneClass α] [ha₅ : NeZero 1] {a b : α} : (∀ (p : Point α), a ≤ p.x ↔ p.x ≤ b) ↔ False

@[simp]

theorem Point.forall_le_iff_le_yy_iff₂ {α : Type u_1} [ha₁ : LinearOrder α] [ha₂ : Ring α] [ha₃ : IsOrderedAddMonoid α] [ha₄ : ZeroLEOneClass α] [ha₅ : NeZero 1] {a b : α} : (∀ (p : Point α), a ≤ p.y ↔ p.y ≤ b) ↔ False

@[simp]

theorem Point.forall_le_iff_le_xy_iff₂ {α : Type u_1} [ha₁ : LinearOrder α] [ha₂ : Ring α] [ha₃ : IsOrderedAddMonoid α] [ha₄ : ZeroLEOneClass α] [ha₅ : NeZero 1] {a b : α} : (∀ (p : Point α), a ≤ p.x ↔ p.y ≤ b) ↔ False

@[simp]

theorem Point.forall_le_iff_le_yx_iff₂ {α : Type u_1} [ha₁ : LinearOrder α] [ha₂ : Ring α] [ha₃ : IsOrderedAddMonoid α] [ha₄ : ZeroLEOneClass α] [ha₅ : NeZero 1] {a b : α} : (∀ (p : Point α), a ≤ p.y ↔ p.x ≤ b) ↔ False

@[simp]

theorem Point.forall_le_iff_le_xx_iff₃ {α : Type u_1} [ha₁ : LinearOrder α] [ha₂ : Ring α] [ha₃ : IsOrderedAddMonoid α] [ha₄ : ZeroLEOneClass α] [ha₅ : NeZero 1] {a b : α} : (∀ (p : Point α), p.x ≤ a ↔ b ≤ p.x) ↔ False

@[simp]

theorem Point.forall_le_iff_le_yy_iff₃ {α : Type u_1} [ha₁ : LinearOrder α] [ha₂ : Ring α] [ha₃ : IsOrderedAddMonoid α] [ha₄ : ZeroLEOneClass α] [ha₅ : NeZero 1] {a b : α} : (∀ (p : Point α), p.y ≤ a ↔ b ≤ p.y) ↔ False

@[simp]

theorem Point.forall_le_iff_le_xy_iff₃ {α : Type u_1} [ha₁ : LinearOrder α] [ha₂ : Ring α] [ha₃ : IsOrderedAddMonoid α] [ha₄ : ZeroLEOneClass α] [ha₅ : NeZero 1] {a b : α} : (∀ (p : Point α), p.x ≤ a ↔ b ≤ p.y) ↔ False

@[simp]

theorem Point.forall_le_iff_le_yx_iff₃ {α : Type u_1} [ha₁ : LinearOrder α] [ha₂ : Ring α] [ha₃ : IsOrderedAddMonoid α] [ha₄ : ZeroLEOneClass α] [ha₅ : NeZero 1] {a b : α} : (∀ (p : Point α), p.y ≤ a ↔ b ≤ p.x) ↔ False

@[simp]

theorem Point.forall_le_iff_le_xx_iff₄ {α : Type u_1} [ha₁ : LinearOrder α] [ha₂ : Ring α] {a b : α} : (∀ (p : Point α), a ≤ p.x ↔ b ≤ p.x) ↔ a = b

@[simp]

theorem Point.forall_le_iff_le_yy_iff₄ {α : Type u_1} [ha₁ : LinearOrder α] [ha₂ : Ring α] {a b : α} : (∀ (p : Point α), a ≤ p.y ↔ b ≤ p.y) ↔ a = b

@[simp]

theorem Point.forall_le_iff_le_xy_iff₄ {α : Type u_1} [ha₁ : LinearOrder α] [ha₂ : Ring α] [ha₃ : IsOrderedAddMonoid α] [ha₄ : ZeroLEOneClass α] [ha₅ : NeZero 1] {a b : α} : (∀ (p : Point α), a ≤ p.x ↔ b ≤ p.y) ↔ False

@[simp]

theorem Point.forall_le_iff_le_yx_iff₄ {α : Type u_1} [ha₁ : LinearOrder α] [ha₂ : Ring α] [ha₃ : IsOrderedAddMonoid α] [ha₄ : ZeroLEOneClass α] [ha₅ : NeZero 1] {a b : α} : (∀ (p : Point α), a ≤ p.y ↔ b ≤ p.x) ↔ False

@[simp]

theorem Point.zero_le_dist' {α : Type u_1} [ha₁ : LinearOrder α] [ha₂ : Ring α] [ha₃ : AddLeftMono α] {a b : Point α} : 0 ≤ a.dist b

@[simp]

theorem Point.max_dist_zero {α : Type u_1} [ha₁ : LinearOrder α] [ha₂ : Ring α] [ha₃ : AddLeftMono α] {a b : Point α} : max (a.dist b) 0 = a.dist b

instance Point.instAddLeftMono {α : Type u_1} [ha₁ : LinearOrder α] [ha₂ : Ring α] [ha₃ : AddLeftMono α] : AddLeftMono (Point α)

instance Point.instAddRightMono {α : Type u_1} [ha₁ : LinearOrder α] [ha₂ : Ring α] [ha₃ : AddRightMono α] : AddRightMono (Point α)

theorem Point.forall_iff {α : Type u_1} {p : Point α → Prop} : (∀ (pt : Point α), p pt) ↔ ∀ (x y : α), p { x := x, y := y }

theorem Point.exi_iff {α : Type u_1} {p : Point α → Prop} : (∃ (pt : Point α), p pt) ↔ ∃ (x : α) (y : α), p { x := x, y := y }

@[simp]

theorem Point.nodup_rect {α : Type u_2} [ha₁ : LocallyFiniteOrderList α] [ha₂ : Ring α] {a b c d : α} : (rect a b c d).Nodup

@[simp]

theorem Point.nodup_rectRel {α : Type u_2} [ha₁ : LocallyFiniteOrderList α] [ha₂ : Ring α] {p : Point α} {a b c d : α} : (p.rectRel a b c d).Nodup

@[simp]

theorem Point.nodup_nbhd {α : Type u_2} [ha₁ : LocallyFiniteOrderList α] [ha₂ : Ring α] {p : Point α} {a : α} : (p.nbhd a).Nodup

@[simp]

theorem Point.length_rect_int_nat {p : PointZ} {a b c d : ℕ} : (rect (p.x - ↑a) (p.y - ↑b) (p.x + ↑c) (p.y + ↑d)).length = (a + c + 1) * (b + d + 1)

@[simp]

theorem Point.length_rectRel_int_nat {p : PointZ} {a b c d : ℕ} : (rectRel p ↑a ↑b ↑c ↑d).length = (a + c + 1) * (b + d + 1)

@[simp]

theorem Point.length_nbhd_int_nat {p : PointZ} {n : ℕ} : (nbhd p ↑n).length = (n * 2 + 1) ^ 2

@[simp]

theorem Point.size_set'_ofList_nbhd_int_nat {p : PointZ} {n : ℕ} : (Set'.ofList (nbhd p ↑n)).size = (n * 2 + 1) ^ 2

@[simp]

theorem Point.dist_pos_iff_ne {α : Type u_1} [ha₁ : Ring α] [ha₂ : LinearOrder α] [ha₃ : IsOrderedAddMonoid α] {a b : Point α} : 0 < a.dist b ↔ a ≠ b