EuclideanGeometry.Foundation.Axiom.Triangle.Similarity

source

structure EuclidGeom.IsSim {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr₁ : EuclidGeom.TriangleND P) (tr₂ : EuclidGeom.TriangleND P) :

Prop

The relation of two triangle being similar to each other, i.e. each angle is equal to the corresponding angle.

intro :: (

angle₁ : tr₁.angle₁.value = tr₂.angle₁.value
angle₂ : tr₁.angle₂.value = tr₂.angle₂.value
angle₃ : tr₁.angle₃.value = tr₂.angle₃.value

)

Instances For

source

structure EuclidGeom.IsASim {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr₁ : EuclidGeom.TriangleND P) (tr₂ : EuclidGeom.TriangleND P) :

Prop

The relation of two triangle being anti-similar to each other, i.e. each angle is equal to the negative of corresponding angle.

intro :: (

angle₁ : tr₁.angle₁.value = -tr₂.angle₁.value
angle₂ : tr₁.angle₂.value = -tr₂.angle₂.value
angle₃ : tr₁.angle₃.value = -tr₂.angle₃.value

)

Instances For

source

theorem EuclidGeom.IsSim.refl {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr : EuclidGeom.TriangleND P) :

EuclidGeom.IsSim tr tr

source

theorem EuclidGeom.IsSim.symm {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr₁ : EuclidGeom.TriangleND P} {tr₂ : EuclidGeom.TriangleND P} (h : EuclidGeom.IsSim tr₁ tr₂) :

EuclidGeom.IsSim tr₂ tr₁

source

theorem EuclidGeom.IsSim.trans {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr₁ : EuclidGeom.TriangleND P} {tr₂ : EuclidGeom.TriangleND P} {tr₃ : EuclidGeom.TriangleND P} (h₁ : EuclidGeom.IsSim tr₁ tr₂) (h₂ : EuclidGeom.IsSim tr₂ tr₃) :

EuclidGeom.IsSim tr₁ tr₃

source

instance EuclidGeom.IsSim.instHasSim {P : Type u_1} [EuclidGeom.EuclideanPlane P] :

EuclidGeom.HasSim (EuclidGeom.TriangleND P)

Equations

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

source

theorem EuclidGeom.IsSim.perm_sim {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr₁ : EuclidGeom.TriangleND P} {tr₂ : EuclidGeom.TriangleND P} (h : EuclidGeom.IsSim tr₁ tr₂) :

EuclidGeom.IsSim (EuclidGeom.TriangleND.perm_vertices tr₁) (EuclidGeom.TriangleND.perm_vertices tr₂)

source

theorem EuclidGeom.IsSim.sim_iff_perm_sim {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr₁ : EuclidGeom.TriangleND P} {tr₂ : EuclidGeom.TriangleND P} :

EuclidGeom.IsSim tr₁ tr₂ ↔ EuclidGeom.IsSim (EuclidGeom.TriangleND.perm_vertices tr₁) (EuclidGeom.TriangleND.perm_vertices tr₂)

source

theorem EuclidGeom.IsSim.is_cclock_of_cclock {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr₁ : EuclidGeom.TriangleND P} {tr₂ : EuclidGeom.TriangleND P} (h : EuclidGeom.IsSim tr₁ tr₂) (cc : tr₁.is_cclock) :

tr₂.is_cclock

source

def EuclidGeom.IsSim.ratio {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr₁ : EuclidGeom.TriangleND P} {tr₂ : EuclidGeom.TriangleND P} (_h : EuclidGeom.IsSim tr₁ tr₂) :

ℝ

Equations

EuclidGeom.IsSim.ratio _h = tr₁.edge₁.length / tr₂.edge₁.length

Instances For

source

theorem EuclidGeom.IsSim.ratio₁ {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr₁ : EuclidGeom.TriangleND P} {tr₂ : EuclidGeom.TriangleND P} (h : EuclidGeom.IsSim tr₁ tr₂) :

EuclidGeom.IsSim.ratio h = tr₁.edge₁.length / tr₂.edge₁.length

source

theorem EuclidGeom.IsSim.ratio₂ {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr₁ : EuclidGeom.TriangleND P} {tr₂ : EuclidGeom.TriangleND P} (h : EuclidGeom.IsSim tr₁ tr₂) :

EuclidGeom.IsSim.ratio h = tr₁.edge₂.length / tr₂.edge₂.length

source

theorem EuclidGeom.IsSim.ratio₃ {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr₁ : EuclidGeom.TriangleND P} {tr₂ : EuclidGeom.TriangleND P} (h : EuclidGeom.IsSim tr₁ tr₂) :

EuclidGeom.IsSim.ratio h = tr₁.edge₃.length / tr₂.edge₃.length

source

theorem EuclidGeom.IsSim.ratio₁₂ {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr₁ : EuclidGeom.TriangleND P} {tr₂ : EuclidGeom.TriangleND P} (h : EuclidGeom.IsSim tr₁ tr₂) :

tr₁.edge₁.length / tr₁.edge₂.length = tr₂.edge₁.length / tr₂.edge₂.length

source

theorem EuclidGeom.IsSim.ratio₂₃ {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr₁ : EuclidGeom.TriangleND P} {tr₂ : EuclidGeom.TriangleND P} (h : EuclidGeom.IsSim tr₁ tr₂) :

tr₁.edge₂.length / tr₁.edge₃.length = tr₂.edge₂.length / tr₂.edge₃.length

source

theorem EuclidGeom.IsSim.ratio₃₁ {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr₁ : EuclidGeom.TriangleND P} {tr₂ : EuclidGeom.TriangleND P} (h : EuclidGeom.IsSim tr₁ tr₂) :

tr₁.edge₃.length / tr₁.edge₁.length = tr₂.edge₃.length / tr₂.edge₁.length

source

theorem EuclidGeom.IsSim.oarea {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr₁ : EuclidGeom.TriangleND P} {tr₂ : EuclidGeom.TriangleND P} (h : EuclidGeom.IsSim tr₁ tr₂) :

tr₁.oarea / tr₂.oarea = EuclidGeom.IsSim.ratio h ^ 2

source

theorem EuclidGeom.IsSim.area {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr₁ : EuclidGeom.TriangleND P} {tr₂ : EuclidGeom.TriangleND P} (h : EuclidGeom.IsSim tr₁ tr₂) :

tr₁.area / tr₂.area = EuclidGeom.IsSim.ratio h ^ 2

source

theorem EuclidGeom.IsASim.symm {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr₁ : EuclidGeom.TriangleND P} {tr₂ : EuclidGeom.TriangleND P} (h : EuclidGeom.IsASim tr₁ tr₂) :

EuclidGeom.IsASim tr₂ tr₁

source

instance EuclidGeom.IsASim.instHasASim {P : Type u_1} [EuclidGeom.EuclideanPlane P] :

EuclidGeom.HasASim (EuclidGeom.TriangleND P)

Equations

EuclidGeom.IsASim.instHasASim = { asim := EuclidGeom.IsASim, symm := (_ : ∀ {a b : EuclidGeom.TriangleND P}, EuclidGeom.IsASim a b → EuclidGeom.IsASim b a) }

source

theorem EuclidGeom.IsASim.not_cclock_of_cclock {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr₁ : EuclidGeom.TriangleND P} {tr₂ : EuclidGeom.TriangleND P} (h : EuclidGeom.IsASim tr₁ tr₂) (cc : tr₁.is_cclock) :

¬tr₂.is_cclock

source

def EuclidGeom.IsASim.ratio {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr₁ : EuclidGeom.TriangleND P} {tr₂ : EuclidGeom.TriangleND P} (_h : EuclidGeom.IsASim tr₁ tr₂) :

ℝ

Equations

EuclidGeom.IsASim.ratio _h = tr₁.edge₁.length / tr₂.edge₁.length

Instances For

source

theorem EuclidGeom.IsASim.perm_asim {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr₁ : EuclidGeom.TriangleND P} {tr₂ : EuclidGeom.TriangleND P} (h : EuclidGeom.IsASim tr₁ tr₂) :

EuclidGeom.IsASim (EuclidGeom.TriangleND.perm_vertices tr₁) (EuclidGeom.TriangleND.perm_vertices tr₂)

source

theorem EuclidGeom.IsASim.asim_iff_perm_asim {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr₁ : EuclidGeom.TriangleND P} {tr₂ : EuclidGeom.TriangleND P} :

EuclidGeom.IsASim tr₁ tr₂ ↔ EuclidGeom.IsASim (EuclidGeom.TriangleND.perm_vertices tr₁) (EuclidGeom.TriangleND.perm_vertices tr₂)

source

theorem EuclidGeom.IsASim.ratio₁ {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr₁ : EuclidGeom.TriangleND P} {tr₂ : EuclidGeom.TriangleND P} (h : EuclidGeom.IsASim tr₁ tr₂) :

EuclidGeom.IsASim.ratio h = tr₁.edge₁.length / tr₂.edge₁.length

source

theorem EuclidGeom.IsASim.ratio₂ {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr₁ : EuclidGeom.TriangleND P} {tr₂ : EuclidGeom.TriangleND P} (h : EuclidGeom.IsASim tr₁ tr₂) :

EuclidGeom.IsASim.ratio h = tr₁.edge₂.length / tr₂.edge₂.length

source

theorem EuclidGeom.IsASim.ratio₃ {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr₁ : EuclidGeom.TriangleND P} {tr₂ : EuclidGeom.TriangleND P} (h : EuclidGeom.IsASim tr₁ tr₂) :

EuclidGeom.IsASim.ratio h = tr₁.edge₃.length / tr₂.edge₃.length

source

theorem EuclidGeom.IsASim.ratio₁₂ {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr₁ : EuclidGeom.TriangleND P} {tr₂ : EuclidGeom.TriangleND P} (h : EuclidGeom.IsASim tr₁ tr₂) :

tr₁.edge₁.length / tr₁.edge₂.length = tr₂.edge₁.length / tr₂.edge₂.length

source

theorem EuclidGeom.IsASim.ratio₂₃ {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr₁ : EuclidGeom.TriangleND P} {tr₂ : EuclidGeom.TriangleND P} (h : EuclidGeom.IsASim tr₁ tr₂) :

tr₁.edge₂.length / tr₁.edge₃.length = tr₂.edge₂.length / tr₂.edge₃.length

source

theorem EuclidGeom.IsASim.ratio₃₁ {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr₁ : EuclidGeom.TriangleND P} {tr₂ : EuclidGeom.TriangleND P} (h : EuclidGeom.IsASim tr₁ tr₂) :

tr₁.edge₃.length / tr₁.edge₁.length = tr₂.edge₃.length / tr₂.edge₁.length

source

theorem EuclidGeom.IsASim.oarea {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr₁ : EuclidGeom.TriangleND P} {tr₂ : EuclidGeom.TriangleND P} (h : EuclidGeom.IsASim tr₁ tr₂) :

tr₁.oarea / tr₂.oarea = -EuclidGeom.IsASim.ratio h ^ 2

source

theorem EuclidGeom.IsASim.area {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr₁ : EuclidGeom.TriangleND P} {tr₂ : EuclidGeom.TriangleND P} (h : EuclidGeom.IsASim tr₁ tr₂) :

tr₁.area / tr₂.area = EuclidGeom.IsASim.ratio h ^ 2

source

theorem EuclidGeom.sim_of_asim_asim {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr₁ : EuclidGeom.TriangleND P} {tr₂ : EuclidGeom.TriangleND P} {tr₃ : EuclidGeom.TriangleND P} (h₁ : EuclidGeom.IsASim tr₁ tr₂) (h₂ : EuclidGeom.IsASim tr₂ tr₃) :

EuclidGeom.IsSim tr₁ tr₃

source

theorem EuclidGeom.asim_of_sim_asim {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr₁ : EuclidGeom.TriangleND P} {tr₂ : EuclidGeom.TriangleND P} {tr₃ : EuclidGeom.TriangleND P} (h₁ : EuclidGeom.IsSim tr₁ tr₂) (h₂ : EuclidGeom.IsASim tr₂ tr₃) :

EuclidGeom.IsASim tr₁ tr₃

source

theorem EuclidGeom.asim_of_asim_sim {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr₁ : EuclidGeom.TriangleND P} {tr₂ : EuclidGeom.TriangleND P} {tr₃ : EuclidGeom.TriangleND P} (h₁ : EuclidGeom.IsASim tr₁ tr₂) (h₂ : EuclidGeom.IsSim tr₂ tr₃) :

EuclidGeom.IsASim tr₁ tr₃

source

theorem EuclidGeom.sim_of_AA {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr₁ : EuclidGeom.TriangleND P) (tr₂ : EuclidGeom.TriangleND P) (h₂ : tr₁.angle₂.value = tr₂.angle₂.value) (h₃ : tr₁.angle₃.value = tr₂.angle₃.value) :

EuclidGeom.HasSim.sim tr₁ tr₂

source

theorem EuclidGeom.asim_of_AA {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr₁ : EuclidGeom.TriangleND P) (tr₂ : EuclidGeom.TriangleND P) (h₂ : tr₁.angle₂.value = -tr₂.angle₂.value) (h₃ : tr₁.angle₃.value = -tr₂.angle₃.value) :

EuclidGeom.HasASim.asim tr₁ tr₂

source

theorem EuclidGeom.sim_of_SAS {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr₁ : EuclidGeom.TriangleND P) (tr₂ : EuclidGeom.TriangleND P) (e : tr₁.edge₂.length / tr₂.edge₂.length = tr₁.edge₃.length / tr₂.edge₃.length) (a : tr₁.angle₁.value = tr₂.angle₁.value) :

EuclidGeom.HasSim.sim tr₁ tr₂

source

theorem EuclidGeom.asim_of_SAS {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr₁ : EuclidGeom.TriangleND P) (tr₂ : EuclidGeom.TriangleND P) (e : tr₁.edge₂.length / tr₂.edge₂.length = tr₁.edge₃.length / tr₂.edge₃.length) (a : tr₁.angle₁.value = -tr₂.angle₁.value) :

EuclidGeom.HasASim.asim tr₁ tr₂

source

theorem EuclidGeom.TriangleND.IsCongr.IsSim {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr₁ : EuclidGeom.TriangleND P} {tr₂ : EuclidGeom.TriangleND P} (h : EuclidGeom.TriangleND.IsCongr tr₁ tr₂) :

EuclidGeom.IsSim tr₁ tr₂

source

theorem EuclidGeom.IsSim.congr_of_ratio_eq_one {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr₁ : EuclidGeom.TriangleND P} {tr₂ : EuclidGeom.TriangleND P} (h : EuclidGeom.IsSim tr₁ tr₂) (hr : EuclidGeom.IsSim.ratio h = 1) :

EuclidGeom.TriangleND.IsCongr tr₁ tr₂

source

theorem EuclidGeom.TriangleND.IsACongr.IsASim {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr₁ : EuclidGeom.TriangleND P} {tr₂ : EuclidGeom.TriangleND P} (h : EuclidGeom.TriangleND.IsACongr tr₁ tr₂) :

EuclidGeom.IsASim tr₁ tr₂

source

theorem EuclidGeom.IsASim.acongr_of_ratio_eq_one {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr₁ : EuclidGeom.TriangleND P} {tr₂ : EuclidGeom.TriangleND P} (h : EuclidGeom.IsASim tr₁ tr₂) (hr : EuclidGeom.IsASim.ratio h = 1) :

EuclidGeom.TriangleND.IsACongr tr₁ tr₂