Dynamically Verifiable Documentation of Mathematics using Mizar

Mizar を用いた動的検証可能な数学ドキュメンテーション

User Tools

Site Tools


en:example

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revisionPrevious revision
Next revision
Previous revision
en:example [2025/04/08 03:16] – [1.1 TARSKI.miz] superuseren:example [2025/04/08 03:19] (current) – [1.1.4 Definition of the Union of Sets] superuser
Line 43: Line 43:
 \(x, y, z, u, N, M, X, Y, Z\) are arbitrary sets. In set theory, the objects under  \(x, y, z, u, N, M, X, Y, Z\) are arbitrary sets. In set theory, the objects under 
 consideration are either sets or their elements; however, sets and elements are not  consideration are either sets or their elements; however, sets and elements are not 
-formally distinguished. Thus, the term 'setdenotes an arbitrary object.+formally distinguished. Thus, the term set” denotes an arbitrary object.
  
 <mizar ta> <mizar ta>
Line 167: Line 167:
 </mizar> </mizar>
  
-For any \(X\), the functor (operation) \(\cup X\) is defined as the mapping that associates to \(X\) the set satisfying, for any \(x\) に対して+For any \(X\), the functor (operation) \(\cup X\) is defined as the mapping that associates to \(X\) the set satisfying, for any \(x\)
  
 \[(x \in \cup X) \Leftrightarrow((\exists Y)(x \in Y \land Y \in X)).\] \[(x \in \cup X) \Leftrightarrow((\exists Y)(x \in Y \land Y \in X)).\]
en/example.1744082210.txt.gz · Last modified: 2025/04/08 03:16 by superuser