:: Some Properties of the {S}orgenfrey Line and the {S}orgenfrey Plane
::  by Adam J.J. St. Arnaud and Piotr Rudnicki
::
:: Received April 17, 2013
:: Copyright (c) 2013-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 TOPGEN_6, NUMBERS, SUBSET_1, XXREAL_0, ORDINAL1, FUNCT_1,
      RELAT_1, XBOOLE_0, TARSKI, ZFMISC_1, CARD_3, CARD_1, COMPLEX1, ARYTM_3,
      RCOMP_1, ORDINAL2, STRUCT_0, ARYTM_1, REAL_1, TOPGEN_3, CANTOR_1,
      SETFAM_1, RAT_1, TOPS_1, TOPGEN_1, XXREAL_1, RLVECT_3, PRE_TOPC, CARD_5,
      TOPMETR, METRIZTS;
 notations TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1, SUBSET_1, SETFAM_1, FUNCT_1,
      RELSET_1, ORDINAL1, CARD_1, CARD_2, CARD_3, NUMBERS, XCMPLX_0, COMPLEX1,
      REAL_1, XREAL_0, RAT_1, RCOMP_1, DOMAIN_1, FUNCT_2, STRUCT_0, PRE_TOPC,
      BORSUK_1, TOPS_1, TOPS_2, CANTOR_1, TOPMETR, TOPGEN_1, TOPGEN_3,
      XXREAL_0, METRIZTS;
 constructors WELLORD2, REAL_1, COMPLEX1, CARD_2, RCOMP_1, TOPS_1, TOPGEN_2,
      TOPGEN_1, TOPGEN_3, METRIZTS, TOPGEN_5, TOPGEN_4, ORDINAL1, PCOMPS_1;
 registrations SUBSET_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, RAT_1, CARD_1,
      MEMBERED, STRUCT_0, PRE_TOPC, TOPS_1, BORSUK_1, TOPMETR, RELSET_1,
      METRIZTS, TOPGEN_4, CARD_3, TOPGEN_5;
 requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;


begin

reserve T for TopSpace,
  x, y, a, b, U, Ux, rx for set,
  p, q for Rational,
  F, G for Subset-Family of T,
  Us, I for Subset-Family of Sorgenfrey-line;

registration
  cluster Sorgenfrey-line -> T_2;
end;

theorem :: TOPGEN_6:1
  for x, a, b being Real st x in ].a,b.[
    ex p,r being Rational st x in ].p,r.[ & ].p,r.[ c= ].a,b.[;

registration
  cluster -> Lindelof for SubSpace of R^1;
end;

registration
  cluster Sorgenfrey-line -> Lindelof;
end;

definition
  func Sorgenfrey-plane -> non empty strict TopSpace equals
:: TOPGEN_6:def 1
    [:Sorgenfrey-line, Sorgenfrey-line:];
end;

definition  :: ?  how to do it better
  func real-anti-diagonal -> Subset of [:REAL,REAL:] equals
:: TOPGEN_6:def 2
    {[x,y] where x,y is Real : y = -x};
end;

theorem :: TOPGEN_6:2
  [:RAT,RAT:] is dense Subset of Sorgenfrey-plane;

theorem :: TOPGEN_6:3
  card real-anti-diagonal = continuum;

theorem :: TOPGEN_6:4
  real-anti-diagonal is closed Subset of Sorgenfrey-plane;

theorem :: TOPGEN_6:5
  for A being Subset of Sorgenfrey-plane st A = real-anti-diagonal
    holds Der A is empty;

theorem :: TOPGEN_6:6  :: following TOPGEN_5:42
  for A being Subset of real-anti-diagonal
    holds A is closed Subset of Sorgenfrey-plane;

registration
  cluster Sorgenfrey-plane -> non Lindelof;
end;

registration
  cluster Sorgenfrey-line -> regular;
:: Since Tychonoff -> regular
end;

registration
  cluster Sorgenfrey-line -> normal;
end;

registration
  cluster Sorgenfrey-plane -> non normal;
end;