Comments (4)
Perhaps relatedly, does
A. x e. RR A. y e. RR DECID x =//= y
imply_om e. Omni
?
I just now noticed this is already proven - https://us.metamath.org/ileuni/triap.html plus https://us.metamath.org/ileuni/trilpo.html
from set.mm.
If A. x e. RR DECID x =//= 0
, then you can construct a function as in the hypothesis of ncflop
: take it to be 1 if x is apart from zero.
from set.mm.
I think I got it: Let
from set.mm.
Does
A. x e. RR A. y e. RR DECID x =/= y
?
This one also follows similar to @benjub 's first answer: take f(x)
to be 1
if x != 0
. Then f(0) = 0
(because -. ( 0 =/= 0 )
) and f(x) =/= 0
if x > 0
because this implies x != 0
.
from set.mm.
Related Issues (20)
- should iset.mm have both ax-bndl and ax-i12 ? HOT 2
- Appropriate names for +g and gsum HOT 1
- Appropriate name (and new symbol) for LSSum HOT 4
- Barycentric coordinates HOT 2
- If not equal implies apart, Markov's principle follows HOT 2
- Updating mmset.html HOT 12
- Symbol and token for the class of semigroups HOT 9
- Update of the topological structure overview figure HOT 4
- Can a space filling curve exist in iset.mm? HOT 5
- The sine function is decreasing over [2,4] HOT 17
- Making SymGrp a structure restriction of EndoFMnd HOT 7
- Discourage indirect usage of ax-13? HOT 17
- Hypotheses with an "is a set" property using the universal class _V HOT 5
- Newbie here, I created a proof with mmj2. How do I add the proof to the database HOT 17
- </table> tags in AS's mathbox are outside <html> blocks HOT 3
- Interchanging factors in integrals and sums (Lemmas for AKS) HOT 4
- Contributor code RM is used twice HOT 1
- Feedback from a new user, improvement suggestions. HOT 23
- move polynomial section HOT 6
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from set.mm.