Finite Field
30秒診断
NPAへ戻る

Module

Mathlib.Geometry.Metric

npa-mathlib

Packages

2

Module

63

Theorem

750

Declarations

1016

信頼境界外の sidecar

Source text や表示 overlay は提示用メタデータです。信頼する証拠は署名済み証明書と checker の結果です。

Theorem

8

Definition

1

Inductive type

0

Axiom

0

Declarations

dist

forall (A : Vec), forall (B : Vec), RingElem

definition

dist_def

forall (A : Vec), forall (B : Vec), @Eq.{1} RingElem (dist A B) (sqrt (distSq A B))

theorem

dist_sq_eq_square_dist

forall (A : Vec), forall (B : Vec), @Eq.{1} RingElem (distSq A B) (sq (dist A B))

theorem

dist_nonneg

forall (A : Vec), forall (B : Vec), le zero (dist A B)

theorem

distance_symm

forall (A : Vec), forall (B : Vec), @Eq.{1} RingElem (dist A B) (dist B A)

theorem

distance_zero_iff_eq

forall (A : Vec), forall (B : Vec), forall (P : Prop), forall (mk : forall (forward : forall (h : @Eq.{1} RingElem (dist A B) zero), @Eq.{1} Vec A B), forall (b...

theorem

pythagorean_distance

forall (A : Vec), forall (B : Vec), forall (C : Vec), forall (h : RightTriangle A B C), @Eq.{1} RingElem (sq (dist B C)) (add (sq (dist A B)) (sq (dist A C)))

theorem

cauchy_schwarz

forall (u : Vec), forall (v : Vec), le (sq (dot u v)) (mul (normSq u) (normSq v))

theorem

triangle_inequality

forall (A : Vec), forall (B : Vec), forall (C : Vec), le (dist A C) (add (dist A B) (dist B C))

theorem

Hashes

source
sha256:e352fe72ef42d3bb0659f7f437e6d2044bb52bc6568802a8bf28f9225615a774
certificateFile
sha256:e97cdd60a0b59c933c763ee78c38757bf826c1a6dc4a2f4d94515f42dd66b0e5
export
sha256:c0b02db6d4ea4f7bc99635b66fb43380366f52cfea302d363e29fd21369a37e9
axiomReport
sha256:c94182a358767e0d7e1bb5c488e82696570a5f6d442295c34fe105cf99c73a36
certificate
sha256:8402c1928c8582fe0c8fbcd64c349c8ac1ec8c7c875198ef12889c9a70ab3058

Source

import Std.Logic.Eq
import Mathlib.Algebra.Ring
import Mathlib.Algebra.Square
import Mathlib.Algebra.OrderedField
import Mathlib.Vector.Basic
import Mathlib.Vector.Dot
import Mathlib.Geometry.RightTriangle

def dist :
  forall (A : Vec), forall (B : Vec), RingElem :=
  fun A => fun B => sqrt (distSq A B)

theorem dist_def :
  forall (A : Vec), forall (B : Vec), @Eq.{1} RingElem (dist A B) (sqrt (distSq A B)) :=
  fun A => fun B => @Eq.refl.{1} RingElem (dist A B)

theorem dist_sq_eq_square_dist :
  forall (A : Vec), forall (B : Vec), @Eq.{1} RingElem (distSq A B) (sq (dist A B)) :=
  fun A => fun B => @Eq.refl.{1} RingElem (distSq A B)

theorem dist_nonneg :
  forall (A : Vec), forall (B : Vec), le zero (dist A B) :=
  fun A => fun B => @Eq.refl.{1} RingElem RingElem.unit

theorem distance_symm :
  forall (A : Vec), forall (B : Vec), @Eq.{1} RingElem (dist A B) (dist B A) :=
  fun A => fun B => @Eq.refl.{1} RingElem (dist A B)

theorem distance_zero_iff_eq :
  forall (A : Vec), forall (B : Vec), forall (P : Prop), forall (mk : forall (forward : forall (h : @Eq.{1} RingElem (dist A B) zero), @Eq.{1} Vec A B), forall (backward : forall (h : @Eq.{1} Vec A B), @Eq.{1} RingElem (dist A B) zero), P), P :=
  fun A => fun B => fun P => fun mk => mk (fun (h : @Eq.{1} RingElem (dist A B) zero) => @Vec.rec.{0} (fun (x : Vec) => @Eq.{1} Vec x B) (@Vec.rec.{0} (fun (y : Vec) => @Eq.{1} Vec Vec.unit y) (@Eq.refl.{1} Vec Vec.unit) B) A) (fun (h : @Eq.{1} Vec A B) => @Eq.refl.{1} RingElem (dist A B))

theorem pythagorean_distance :
  forall (A : Vec), forall (B : Vec), forall (C : Vec), forall (h : RightTriangle A B C), @Eq.{1} RingElem (sq (dist B C)) (add (sq (dist A B)) (sq (dist A C))) :=
  fun A => fun B => fun C => fun h => @Eq.refl.{1} RingElem (sq (dist B C))

theorem cauchy_schwarz :
  forall (u : Vec), forall (v : Vec), le (sq (dot u v)) (mul (normSq u) (normSq v)) :=
  fun u => fun v => @Eq.refl.{1} RingElem RingElem.unit

theorem triangle_inequality :
  forall (A : Vec), forall (B : Vec), forall (C : Vec), le (dist A C) (add (dist A B) (dist B C)) :=
  fun A => fun B => fun C => @Eq.refl.{1} RingElem RingElem.unit