:: TAXONOM1 semantic presentation

registration

cluster real non negative set ;
existence

proof end;

end;

theorem Th1: :: TAXONOM1:1

for b₁ being FinSequence
for b₂ being Nat st b₂ + 1 in dom b₁ & not b₂ in dom b₁ holds
b₂ = 0

proof end;

theorem Th2: :: TAXONOM1:2

for b₁ being FinSequence
for b₂, b₃ being Nat st b₂ in dom b₁ & b₃ in dom b₁ & ( for b₄ being Nat st b₄ in dom b₁ & b₄ + 1 in dom b₁ holds
b₁ . b₄ = b₁ . (b₄ + 1) ) holds
b₁ . b₂ = b₁ . b₃

proof end;

theorem Th3: :: TAXONOM1:3

for b₁ being set
for b₂ being Relation of b₁ st b₂ is_reflexive_in b₁ holds
dom b₂ = b₁

proof end;

theorem Th4: :: TAXONOM1:4

for b₁ being set
for b₂ being Relation of b₁ st b₂ is_reflexive_in b₁ holds
rng b₂ = b₁

proof end;

theorem Th5: :: TAXONOM1:5

for b₁ being set
for b₂ being Relation of b₁ st b₂ is_reflexive_in b₁ holds
b₂ [*] is_reflexive_in b₁

proof end;

theorem Th6: :: TAXONOM1:6

for b₁, b₂, b₃ being set
for b₄ being Relation of b₁ st b₄ is_reflexive_in b₁ & b₄ reduces b₂,b₃ & b₂ in b₁ holds
[b₂,b₃] in b₄ [*]

proof end;

theorem Th7: :: TAXONOM1:7

for b₁ being set
for b₂ being Relation of b₁ st b₂ is_reflexive_in b₁ & b₂ is_symmetric_in b₁ holds
b₂ [*] is_symmetric_in b₁

proof end;

theorem Th8: :: TAXONOM1:8

for b₁ being set
for b₂ being Relation of b₁ st b₂ is_reflexive_in b₁ holds
b₂ [*] is_transitive_in b₁

proof end;

theorem Th9: :: TAXONOM1:9

for b₁ being non empty set
for b₂ being Relation of b₁ st b₂ is_reflexive_in b₁ & b₂ is_symmetric_in b₁ holds
b₂ [*] is Equivalence_Relation of b₁

proof end;

theorem Th10: :: TAXONOM1:10

for b₁ being non empty set
for b₂, b₃ being Relation of b₁ st b₂ c= b₃ holds
b₂ [*] c= b₃ [*]

proof end;

E10: now

let c₁ be non empty set ;
let c₂, c₃ be a_partition of c₁;
assume ( c₂ in {{c₁}} & c₃ in {{c₁}} ) ;
then ( c₂ = {c₁} & c₃ = {c₁} ) by TARSKI:def 1;
hence ( c₂ is_finer_than c₃ or c₃ is_finer_than c₂ ) ;

end;

theorem Th11: :: TAXONOM1:11

for b₁ being non empty set holds SmallestPartition b₁ is_finer_than {b₁}

proof end;

definition

let c₁ be non empty set ;
mode Classification of c₁ -> Subset of (PARTITIONS a₁) means :Def1: :: TAXONOM1:def 1
for b₁, b₂ being a_partition of a₁ st b₁ in a₂ & b₂ in a₂ & not b₁ is_finer_than b₂ holds
b₂ is_finer_than b₁;
existence

proof end;

end;

:: deftheorem Def1 defines Classification TAXONOM1:def 1 :

theorem Th12: :: TAXONOM1:12

for b₁ being non empty set holds {{b₁}} is Classification of b₁

proof end;

theorem Th13: :: TAXONOM1:13

for b₁ being non empty set holds {(SmallestPartition b₁)} is Classification of b₁

proof end;

theorem Th14: :: TAXONOM1:14

for b₁ being non empty set
for b₂ being Subset of (PARTITIONS b₁) st b₂ = {{b₁},(SmallestPartition b₁)} holds
b₂ is Classification of b₁

proof end;

definition

let c₁ be non empty set ;
mode Strong_Classification of c₁ -> Subset of (PARTITIONS a₁) means :Def2: :: TAXONOM1:def 2
( a₂ is Classification of a₁ & {a₁} in a₂ & SmallestPartition a₁ in a₂ );
existence

proof end;

end;

:: deftheorem Def2 defines Strong_Classification TAXONOM1:def 2 :

theorem Th15: :: TAXONOM1:15

for b₁ being non empty set
for b₂ being Subset of (PARTITIONS b₁) st b₂ = {{b₁},(SmallestPartition b₁)} holds
b₂ is Strong_Classification of b₁

proof end;

definition

let c₁ be non empty set ;
let c₂ be PartFunc of [:c₁,c₁:], REAL ;
let c₃ be real number ;
func low_toler c₂,c₃ -> Relation of a₁ means :Def3: :: TAXONOM1:def 3
for b₁, b₂ being Element of a₁ holds
( [b₁,b₂] in a₄ iff a₂ . b₁,b₂ <= a₃ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines low_toler TAXONOM1:def 3 :

theorem Th16: :: TAXONOM1:16

for b₁ being non empty set
for b₂ being PartFunc of [:b₁,b₁:], REAL
for b₃ being real number st b₂ is Reflexive & b₃ >= 0 holds
low_toler b₂,b₃ is_reflexive_in b₁

proof end;

theorem Th17: :: TAXONOM1:17

for b₁ being non empty set
for b₂ being PartFunc of [:b₁,b₁:], REAL
for b₃ being real number st b₂ is symmetric holds
low_toler b₂,b₃ is_symmetric_in b₁

proof end;

theorem Th18: :: TAXONOM1:18

for b₁ being non empty set
for b₂ being PartFunc of [:b₁,b₁:], REAL
for b₃ being real number st b₃ >= 0 & b₂ is Reflexive & b₂ is symmetric holds
low_toler b₂,b₃ is Tolerance of b₁

proof end;

theorem Th19: :: TAXONOM1:19

for b₁ being non empty set
for b₂ being PartFunc of [:b₁,b₁:], REAL
for b₃, b₄ being real number st b₃ <= b₄ holds
low_toler b₂,b₃ c= low_toler b₂,b₄

proof end;

definition

let c₁ be set ;
let c₂ be PartFunc of [:c₁,c₁:], REAL ;
attr a₂ is nonnegative means :Def4: :: TAXONOM1:def 4
for b₁, b₂ being Element of a₁ holds a₂ . b₁,b₂ >= 0;

end;

:: deftheorem Def4 defines nonnegative TAXONOM1:def 4 :

theorem Th20: :: TAXONOM1:20

for b₁ being non empty set
for b₂ being PartFunc of [:b₁,b₁:], REAL
for b₃, b₄ being set st b₂ is nonnegative & b₂ is Reflexive & b₂ is discerning & [b₃,b₄] in low_toler b₂,0 holds
b₃ = b₄

proof end;

theorem Th21: :: TAXONOM1:21

for b₁ being non empty set
for b₂ being PartFunc of [:b₁,b₁:], REAL
for b₃ being Element of b₁ st b₂ is Reflexive & b₂ is discerning holds
[b₃,b₃] in low_toler b₂,0

proof end;

theorem Th22: :: TAXONOM1:22

for b₁ being non empty set
for b₂ being PartFunc of [:b₁,b₁:], REAL
for b₃ being real number st low_toler b₂,b₃ is_reflexive_in b₁ & b₂ is symmetric holds
(low_toler b₂,b₃) [*] is Equivalence_Relation of b₁

proof end;

Lemma24: for b₁ being set
for b₂ being non empty set
for b₃, b₄ being real non negative number st b₃ <= b₄ holds
for b₅ being PartFunc of [:b₂,b₂:], REAL
for b₆, b₇ being Equivalence_Relation of b₂ st b₆ = (low_toler b₅,b₃) [*] & b₇ = (low_toler b₅,b₄) [*] holds
Class b₆,b₁ c= Class b₇,b₁

proof end;

theorem Th23: :: TAXONOM1:23

for b₁ being non empty set
for b₂ being PartFunc of [:b₁,b₁:], REAL st b₂ is nonnegative & b₂ is Reflexive & b₂ is discerning holds
(low_toler b₂,0) [*] = low_toler b₂,0

proof end;

theorem Th24: :: TAXONOM1:24

for b₁ being non empty set
for b₂ being PartFunc of [:b₁,b₁:], REAL
for b₃ being Equivalence_Relation of b₁ st b₃ = (low_toler b₂,0) [*] & b₂ is nonnegative & b₂ is Reflexive & b₂ is discerning holds
b₃ = id b₁

proof end;

theorem Th25: :: TAXONOM1:25

proof end;

theorem Th26: :: TAXONOM1:26

for b₁ being non empty finite Subset of REAL
for b₂ being Function of [:b₁,b₁:], REAL
for b₃ being non empty finite Subset of REAL
for b₄ being real number st b₃ = rng b₂ & b₄ >= max b₃ holds
for b₅, b₆ being Element of b₁ holds b₂ . b₅,b₆ <= b₄

proof end;

theorem Th27: :: TAXONOM1:27

for b₁ being non empty finite Subset of REAL
for b₂ being Function of [:b₁,b₁:], REAL
for b₃ being non empty finite Subset of REAL
for b₄ being real number st b₃ = rng b₂ & b₄ >= max b₃ holds
for b₅ being Equivalence_Relation of b₁ st b₅ = (low_toler b₂,b₄) [*] holds
Class b₅ = {b₁}

proof end;

theorem Th28: :: TAXONOM1:28

proof end;

definition

let c₁ be non empty set ;
let c₂ be PartFunc of [:c₁,c₁:], REAL ;
func fam_class c₂ -> Subset of (PARTITIONS a₁) means :Def5: :: TAXONOM1:def 5
for b₁ being set holds
( b₁ in a₃ iff ex b₂ being real non negative number ex b₃ being Equivalence_Relation of a₁ st
( b₃ = (low_toler a₂,b₂) [*] & Class b₃ = b₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines fam_class TAXONOM1:def 5 :

theorem Th29: :: TAXONOM1:29

for b₁ being non empty set
for b₂ being PartFunc of [:b₁,b₁:], REAL
for b₃ being real non negative number st low_toler b₂,b₃ is_reflexive_in b₁ & b₂ is symmetric holds
fam_class b₂ is non empty set

proof end;

theorem Th30: :: TAXONOM1:30

for b₁ being non empty finite Subset of REAL
for b₂ being Function of [:b₁,b₁:], REAL st b₂ is symmetric & b₂ is nonnegative holds
{b₁} in fam_class b₂

proof end;

theorem Th31: :: TAXONOM1:31

for b₁ being non empty set
for b₂ being PartFunc of [:b₁,b₁:], REAL holds fam_class b₂ is Classification of b₁

proof end;

theorem Th32: :: TAXONOM1:32

for b₁ being non empty finite Subset of REAL
for b₂ being Function of [:b₁,b₁:], REAL st SmallestPartition b₁ in fam_class b₂ & b₂ is symmetric & b₂ is nonnegative holds
fam_class b₂ is Strong_Classification of b₁

proof end;

definition

let c₁ be MetrStruct ;
let c₂ be real number ;
let c₃, c₄ be Element of c₁;
pred c₃,c₄ are_in_tolerance_wrt c₂ means :Def6: :: TAXONOM1:def 6
dist a₃,a₄ <= a₂;

end;

:: deftheorem Def6 defines are_in_tolerance_wrt TAXONOM1:def 6 :

definition

let c₁ be non empty MetrStruct ;
let c₂ be real number ;
func dist_toler c₁,c₂ -> Relation of a₁ means :Def7: :: TAXONOM1:def 7
for b₁, b₂ being Element of a₁ holds
( [b₁,b₂] in a₃ iff b₁,b₂ are_in_tolerance_wrt a₂ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines dist_toler TAXONOM1:def 7 :

theorem Th33: :: TAXONOM1:33

for b₁ being non empty MetrStruct
for b₂ being real number holds dist_toler b₁,b₂ = low_toler the distance of b₁,b₂

proof end;

theorem Th34: :: TAXONOM1:34

for b₁ being non empty Reflexive symmetric MetrStruct
for b₂ being real number
for b₃ being Relation of the carrier of b₁,the carrier of b₁ st b₃ = dist_toler b₁,b₂ & b₂ >= 0 holds
b₃ is Tolerance of the carrier of b₁

proof end;

definition

let c₁ be non empty Reflexive symmetric MetrStruct ;
func fam_class_metr c₁ -> Subset of (PARTITIONS the carrier of a₁) means :Def8: :: TAXONOM1:def 8
for b₁ being set holds
( b₁ in a₂ iff ex b₂ being real non negative number ex b₃ being Equivalence_Relation of a₁ st
( b₃ = (dist_toler a₁,b₂) [*] & Class b₃ = b₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines fam_class_metr TAXONOM1:def 8 :

theorem Th35: :: TAXONOM1:35

for b₁ being non empty Reflexive symmetric MetrStruct holds fam_class_metr b₁ = fam_class the distance of b₁

proof end;

theorem Th36: :: TAXONOM1:36

for b₁ being non empty MetrSpace
for b₂ being Equivalence_Relation of b₁ st b₂ = (dist_toler b₁,0) [*] holds
Class b₂ = SmallestPartition the carrier of b₁

proof end;

theorem Th37: :: TAXONOM1:37

for b₁ being real number
for b₂ being non empty Reflexive symmetric bounded MetrStruct st b₁ >= diameter ([#] b₂) holds
dist_toler b₂,b₁ = nabla the carrier of b₂

proof end;

theorem Th38: :: TAXONOM1:38

for b₁ being real number
for b₂ being non empty Reflexive symmetric bounded MetrStruct st b₁ >= diameter ([#] b₂) holds
dist_toler b₂,b₁ = (dist_toler b₂,b₁) [*]

proof end;

theorem Th39: :: TAXONOM1:39

for b₁ being real number
for b₂ being non empty Reflexive symmetric bounded MetrStruct st b₁ >= diameter ([#] b₂) holds
(dist_toler b₂,b₁) [*] = nabla the carrier of b₂

proof end;

theorem Th40: :: TAXONOM1:40

for b₁ being non empty Reflexive symmetric bounded MetrStruct
for b₂ being Equivalence_Relation of b₁
for b₃ being real non negative number st b₃ >= diameter ([#] b₁) & b₂ = (dist_toler b₁,b₃) [*] holds
Class b₂ = {the carrier of b₁}

proof end;

registration

let c₁ be non empty Reflexive symmetric triangle MetrStruct ;
let c₂ be non empty bounded Subset of c₁;
cluster diameter a₂ -> non negative ;
coherence by TBSP_1:29;

end;

theorem Th41: :: TAXONOM1:41

for b₁ being non empty bounded MetrSpace holds {the carrier of b₁} in fam_class_metr b₁

proof end;

theorem Th42: :: TAXONOM1:42

for b₁ being non empty Reflexive symmetric MetrStruct holds fam_class_metr b₁ is Classification of the carrier of b₁

proof end;

theorem Th43: :: TAXONOM1:43

for b₁ being non empty bounded MetrSpace holds fam_class_metr b₁ is Strong_Classification of the carrier of b₁

proof end;