statements) readable to the author of the paper.
Orienteering
------------
+------------
The graphical interface of Matita is composed of three windows:
the script window, on the left, is where you type; the sequent
to mean double or single arrows.
Here we recall some of these "shortcuts":
- - ∀ `\Forall`
- - λ `\lambda`
- - ≝ `\def` or `:=`
- - → `to` or `->`
+ - ∀ can be typed with `\Forall`
+ - λ can be typed with `\lambda`
+ - ≝ can be typed with `\def` or `:=`
+ - → can be typed with `to` or `->`
-- some symbols have variants, like the â\89¤ relation and â\89², â\89¼, â\89°, â\8b .
- The use can cycle between variants typing one them and then
+- some symbols have variants, like the ≤ relation and ≼, ≰, ⋠.
+ The user can cycle between variants typing one of them and then
pressing ALT-L. Note that also letters do have variants, for
example W has Ω, 𝕎 and 𝐖, L has Λ, 𝕃, and 𝐋, F has Φ, …
Variants are listed in the aforementioned TeX/UTF-8 table.
alias symbol "covers" = "new covers set".
alias symbol "covers" = "new covers".
alias symbol "covers" = "new covers set".
+alias symbol "covers" = "new covers".
+alias symbol "covers" = "new covers set".
+alias symbol "covers" = "new covers".
ntheorem new_coverage_infinity:
∀A:nAx.∀U:Ω^A.∀a:A. (∃i:𝐈 a. 𝐈𝐦[𝐝 a i] ◃ U) → a ◃ U.
#A; #U; #a; (** screenshot "n-cov-inf-1". *)
D*)
ntheorem max_new_fished:
- ∀A:nAx.∀G:qpowerclass_setoid A.∀F:Ω^A.G ⊆ F → (∀a.a ∈ G → ∀i.𝐈𝐦[𝐝 a i] ≬ G) → G ⊆ ⋉F.
+ ∀A:nAx.∀G:ext_powerclass_setoid A.∀F:Ω^A.G ⊆ F → (∀a.a ∈ G → ∀i.𝐈𝐦[𝐝 a i] ≬ G) → G ⊆ ⋉F.
#A; #G; #F; #GF; #H; #b; #HbG; #o;
ngeneralize in match HbG; ngeneralize in match b;
nchange with (G ⊆ F⎽o);
##| #p; #IH; napply (subseteq_intersection_r … IH);
#x; #Hx; #i; ncases (H … Hx i); #c; *; *; #d; #Ed; #cG;
@d; napply IH;
- napply (. Ed^-1‡#); napply cG;
+ alias symbol "prop2" = "prop21".
+napply (. Ed^-1‡#); napply cG;
##| #a; #i; #f; #Hf; nchange with (G ⊆ { y | ∀x. y ∈ F⎽(f x) });
#b; #Hb; #d; napply (Hf d); napply Hb;
##]