User talk:GrzegorzBancerek

Welcome to ProofWiki! Since you're new, you may want to check out the general help page. It's the best first stop to see how things are done (next to reading proofs, of course!). Please feel free to contribute to whichever area of mathematics interests you, either by adding new proofs, or fixing up existing ones. If you have any questions please feel free to contact one of the administrators, or post your question on the questions page.

Here are some useful pages to help get you started:

• Community Portal - To see what needs to be done, and keep up to date with the community.
• Recent Changes - To keep up with what's new, and what's being added.
• Check out our house style if you are keen on contributing.
• Main Page talk - This is where most of the main discussions regarding the direction of the site take place. If you have any ideas, please share them!

Cheers! prime mover (talk) 21:26, 12 November 2015 (UTC)

Topology work

You will notice that I have done some rework on the pages you have added. This is because we have a detailed and tightly-controlled house style (both in presentation of material and structure of source code), which you will become familiar with as work progresses.

You may wish to amend the citations under the "Sources" heading to the Engelking work to reference the revised edition of 1989, if that is the one you are using. If this is the case, then please replace all instances of:

{{BookReference|General Topology|1977|Ryszard Engelking}}

with:

{{BookReference|General Topology|1989|Ryszard Engelking|ed = revised and completed|edpage = Revised and Completed Edition}}

I would also like to suggest that you include an indication of the chapter / section / item number in the work (as appropriate) that each page references.

Also note the template that can (and should) be used for referencing Mizar.

I am thinking about the differences in definition of derived set / set derivative, and whether the reference to "accumulation point" is in fact the same thing as "limit point". When I decide how to resolve this, I will refactor the pages in question to match the house style that has evolved.

Many thanks for this excellent work. --prime mover (talk) 22:44, 19 December 2015 (UTC)

Mizar "YELLOW"

I noticed you started work on a new series of Mizar articles under the moniker "YELLOW". Please note that these articles seem to have some specific interpretation of Definition:Join Semilattice in mind, as remarked on Preceding iff Join equals Larger Operand.

This needs to be taken into account, preferably by first setting up the proper equivalence proofs before proceeding any further. This will ensure consistency and prevent any undesired confluence or clash of terminology. There have been painstaking instances in the past (and probably still) where two approaches from different directions obstructed proper coverage of a subject because of these issues (the situation with Takeuti/Zaring set theory vs. the other pages is similar).

That being said, thanks for your continued high-quality contributions, which need pleasingly little adjustment to fit the desired ProofWiki expository style. — Lord_Farin (talk) 17:57, 9 August 2016 (UTC)

Thanks for being a great contributor

We've added you to our trusted users group. This group will give you many more privileges including the ability to delete pages. See here for a complete list. Again, thanks for being a great contributor and member of the ProofWiki community. --Joe (talk) 14:03, 24 October 2016 (EDT)

Page requests on finite subsets and ideals

In Elements of Finite Support form Submagma of Direct Product, I needed the fact that the finite subsets of a set form an ideal. I'm not sure if there already exists a page with a proof of that; I thougt you'd know. (Note that there is Finite Subsets form Directed Set.)

Also, there is Definition:Filter and Definition:Filter on Set, and Definition:Ideal (Order Theory) but not Definition:Ideal of Set (which I'd expect there to be, in analogy with filters). It would be nice if you'd write a few words about that. (I won't try as I might not use the correct terminology and mess it up.) --barto (talk) 18:12, 16 December 2016 (EST)

Mizar YELLOW_0:22, i.e. Alternative Definition of Join

I was looking into refactoring this according to the template. However, the similarity with Definition:Join (Order Theory) (and so, Definition 1) was striking.

In fact, the only difference I was able to find also in following the Mizar structure, was that Th22 formulates in terms of a combination of $\preceq$ and $\succeq$, while the definition of join exclusively deals with $\preceq$. This subtle yet superfluous distinction (the elementary equivalence of $a \preceq b$ and $b \succeq a$ has been demonstrated already on this site) does not seem to me to warrant the continued existence of this page. What do you say? — Lord_Farin (talk) 16:43, 30 August 2017 (EDT)

(NB. The same applies to Alternative Definition of Meet — Lord_Farin (talk) 16:46, 30 August 2017 (EDT))

Due to the lack of a response here, I have proceeded to dispose of both pages. — Lord_Farin (talk) 15:38, 4 September 2017 (EDT)