:: The {F}ashoda Meet Theorem for Continuous Mappings
::  by Yatsuka Nakamura , Andrzej Trybulec and Artur Korni{\l}owicz
::
:: Received September 14, 2005
:: Copyright (c) 2005-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, SUBSET_1, PRE_TOPC, EUCLID, BORSUK_1, PCOMPS_1, TOPMETR,
      CARD_1, FINSEQ_1, XXREAL_0, ORDINAL4, FUNCT_1, ARYTM_3, RELAT_1,
      PARTFUN1, ORDINAL2, ARYTM_1, JGRAPH_6, CONVEX1, MCART_1, RLTOPSP1,
      REAL_1, TOPREALA, TARSKI, STRUCT_0, XXREAL_1, MEASURE5, XBOOLE_0,
      FCONT_2, METRIC_1, NAT_1, INT_1, COMPLEX1, XXREAL_2, RELAT_2, RCOMP_1,
      CONNSP_1, GRAPH_1, WEIERSTR, PSCOMP_1, GOBOARD1, GOBOARD4, TOPREAL1,
      BORSUK_2;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0,
      XREAL_0, COMPLEX1, REAL_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2,
      FINSEQ_1, NAT_1, NAT_D, SEQM_3, STRUCT_0, TOPREAL1, PRE_TOPC, GOBOARD1,
      GOBOARD4, TOPMETR, PCOMPS_1, COMPTS_1, WEIERSTR, METRIC_1, TBSP_1,
      RCOMP_1, UNIFORM1, INT_1, CONNSP_1, PSCOMP_1, RLVECT_1, RLTOPSP1, EUCLID,
      BORSUK_1, BORSUK_2, JGRAPH_6, TOPREALA, TOPALG_2;
 constructors REAL_1, RCOMP_1, CONNSP_1, COMPTS_1, TBSP_1, TOPREAL1, GOBOARD1,
      GOBOARD4, PSCOMP_1, WEIERSTR, UNIFORM1, JGRAPH_6, TOPALG_2, TOPREALA,
      BORSUK_2, NAT_D, XXREAL_2, FUNCSDOM, CONVEX1, BINOP_2, NUMBERS;
 registrations RELAT_1, XREAL_0, INT_1, FINSEQ_1, STRUCT_0, PRE_TOPC, BORSUK_1,
      EUCLID, TOPREAL1, BORSUK_2, JORDAN5A, TOPALG_2, MEMBERED, VALUED_0,
      FUNCT_2, XXREAL_2, RELSET_1, SPPOL_1, TOPMETR, FUNCT_1, NAT_1, ORDINAL1;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;


begin

reserve x, y for set;
reserve i, j, n for Nat;
reserve p1, p2 for Point of TOP-REAL n;
reserve a, b, c, d for Real;

registration
  let a, b, c, d;
  cluster closed_inside_of_rectangle(a,b,c,d) -> convex;
end;

registration
  let a, b, c, d;
  cluster Trectangle(a,b,c,d) -> convex;
end;

theorem :: JGRAPH_8:1
  for e being positive Real, g being continuous Function
  of I[01],TOP-REAL n ex h being FinSequence of REAL st h.1=0 & h.len h=1 & 5<=
len h & rng h c= the carrier of I[01] & h is increasing &
   (for i being Nat,Q being Subset of I[01], W being Subset of Euclid n
    st 1<=i & i<len h &
  Q=[.h/.i,h/.(i+1).] & W=g.:(Q) holds diameter(W)<e);

theorem :: JGRAPH_8:2
  for P being Subset of TOP-REAL n st P c= LSeg(p1,p2) & p1 in P &
  p2 in P & P is connected holds P = LSeg(p1,p2);

theorem :: JGRAPH_8:3
  for g being Path of p1,p2 st rng g c= LSeg(p1,p2) holds rng g = LSeg(p1,p2);

:: Goboard Theorem in continuous case

theorem :: JGRAPH_8:4
  for P, Q being non empty Subset of TOP-REAL 2, p1, p2, q1, q2
being Point of TOP-REAL 2, f being Path of p1,p2, g being Path of q1,q2 st rng
f = P & rng g = Q & (for p being Point of TOP-REAL 2 st p in P holds p1`1<=p`1
& p`1<= p2`1) & (for p being Point of TOP-REAL 2 st p in Q holds p1`1<=p`1 & p
`1<= p2`1) & (for p being Point of TOP-REAL 2 st p in P holds q1`2<=p`2 & p`2<=
q2`2) & (for p being Point of TOP-REAL 2 st p in Q holds q1`2<=p`2 & p`2<= q2`2
  ) holds P meets Q;

:: Fashoda Meet Theorem

theorem :: JGRAPH_8:5
  for f,g being continuous Function of I[01],TOP-REAL 2, O,I being
Point of I[01] st O=0 & I=1 & (f.O)`1=a & (f.I)`1=b & (g.O)`2=c & (g.I)`2=d & (
for r being Point of I[01] holds a <=(f.r)`1 & (f.r)`1<=b & a <=(g.r)`1 & (g.r)
`1<=b & c <=(f.r)`2 & (f.r)`2<=d & c <=(g.r)`2 & (g.r)`2<=d) holds rng f meets
  rng g;

theorem :: JGRAPH_8:6
  for ar, br, cr, dr being Point of Trectangle(a,b,c,d) for h being Path
of ar,br, v being Path of dr,cr for Ar, Br, Cr, Dr being Point of TOP-REAL 2 st
Ar`1 = a & Br`1 = b & Cr`2 = c & Dr`2 = d & ar = Ar & br = Br & cr = Cr & dr =
  Dr ex s, t being Point of I[01] st h.s = v.t;