let X be non empty finite Subset of REAL; for f being Function of [:X,X:],REAL
for z being non empty finite Subset of REAL
for A being Real st z = rng f & A >= max z holds
for R being Equivalence_Relation of X st R = (low_toler (f,A)) [*] holds
Class R = {X}
let f be Function of [:X,X:],REAL; for z being non empty finite Subset of REAL
for A being Real st z = rng f & A >= max z holds
for R being Equivalence_Relation of X st R = (low_toler (f,A)) [*] holds
Class R = {X}
let z be non empty finite Subset of REAL; for A being Real st z = rng f & A >= max z holds
for R being Equivalence_Relation of X st R = (low_toler (f,A)) [*] holds
Class R = {X}
let A be Real; ( z = rng f & A >= max z implies for R being Equivalence_Relation of X st R = (low_toler (f,A)) [*] holds
Class R = {X} )
assume A1:
( z = rng f & A >= max z )
; for R being Equivalence_Relation of X st R = (low_toler (f,A)) [*] holds
Class R = {X}
now for R being Equivalence_Relation of X st R = (low_toler (f,A)) [*] holds
Class R = {X}let R be
Equivalence_Relation of
X;
( R = (low_toler (f,A)) [*] implies Class R = {X} )assume A2:
R = (low_toler (f,A)) [*]
;
Class R = {X}A3:
for
x being
set st
x in X holds
X = Class (
R,
x)
proof
let x be
set ;
( x in X implies X = Class (R,x) )
assume
x in X
;
X = Class (R,x)
then reconsider x9 =
x as
Element of
X ;
now for x1 being object st x1 in X holds
x1 in Class (R,x)let x1 be
object ;
( x1 in X implies x1 in Class (R,x) )assume
x1 in X
;
x1 in Class (R,x)then reconsider x19 =
x1 as
Element of
X ;
f . (
x19,
x9)
<= A
by A1, Th26;
then A4:
[x1,x] in low_toler (
f,
A)
by Def3;
low_toler (
f,
A)
c= (low_toler (f,A)) [*]
by LANG1:18;
hence
x1 in Class (
R,
x)
by A2, A4, EQREL_1:19;
verum end;
then
X c= Class (
R,
x)
;
hence
X = Class (
R,
x)
by XBOOLE_0:def 10;
verum
end; then A7:
{X} c= Class R
;
then
Class R c= {X}
;
hence
Class R = {X}
by A7, XBOOLE_0:def 10;
verum end;
hence
for R being Equivalence_Relation of X st R = (low_toler (f,A)) [*] holds
Class R = {X}
; verum