Skip to content

Mathbox constructible set additions - #5547

Open
BTernaryTau wants to merge 22 commits into
metamath:developfrom
BTernaryTau:construct
Open

BTernaryTau wants to merge 22 commits into
metamath:developfrom
BTernaryTau:construct

Conversation

@BTernaryTau

Copy link
Copy Markdown
Contributor

Highlights:

  • jf1o: _J is a bijection from ( ( On X. On ) X. 9o ) to On . Proposition 15.3 of [TakeutiZaring] p. 155.
  • jk1k2k3: Identity law for the _J function. Proposition 15.8 of [TakeutiZaring] p. 156.
  • k1le: The value of _K1 is bounded by its argument. Part of Proposition 15.10(1) of [TakeutiZaring] p. 156.
  • k2le: The value of _K2 is bounded by its argument. Part of Proposition 15.10(1) of [TakeutiZaring] p. 156.
  • k3n0k1lt: The value of _K1 is strictly bounded by its argument when the value of _K3 is nonzero. Part of Proposition 15.10(2) of [TakeutiZaring] p. 156.
  • k3n0k2lt: The value of _K2 is strictly bounded by its argument when the value of _K3 is nonzero. Part of Proposition 15.10(2) of [TakeutiZaring] p. 156.
  • jltaleph: The value of _J is less than an aleph if its first two arguments are less than that aleph. Proposition 15.11 of [TakeutiZaring] p. 156.
  • fnlfvk30: The value of _FL when the value of _K3 is zero. Part of Proposition 15.14 of [TakeutiZaring] p. 158.
  • fnlfvk3n0: The value of _FL when the value of _K3 is nonzero. Part of Proposition 15.14 of [TakeutiZaring] p. 158.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants