-
Notifications
You must be signed in to change notification settings - Fork 299
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
feat(set_theory/cardinal): more lemmas on cardinality #595
feat(set_theory/cardinal): more lemmas on cardinality #595
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Just some stylistic comments
data/set/basic.lean
Outdated
@@ -823,6 +823,10 @@ theorem image_inter {f : α → β} {s t : set α} (H : injective f) : | |||
f '' s ∩ f '' t = f '' (s ∩ t) := | |||
image_inter_on (assume x _ y _ h, H h) | |||
|
|||
theorem surjective_onto_image {f : α → β} {s : set α} : | |||
surjective (λ p, ⟨f p.1, ⟨p.1, p.2, rfl⟩⟩ : s → f '' s) := |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It would be nicer to use the lemma mem_image_of_mem
(like mem_range_self
) in the later proof.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think this function should be given a name, so that the proofs don't appear in the statement of the theorem.
set_theory/cardinal.lean
Outdated
exact subtype.mk.inj (eq_of_heq H2) | ||
end⟩⟩ | ||
≤ mk (Σ i, f i) : mk_le_of_surjective $ show surjective | ||
(show (Σ i, f i) → (⋃ i, f i), from λ ⟨i, x, hx⟩, ⟨x, mem_Union.2 ⟨i, hx⟩⟩), from |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think the proof would be nicer as (NOTE: I didn't test this proof)
let f : (Σ i, f i) → (⋃ i, f i) := λ ⟨i, x, hx⟩, ⟨x, mem_Union.2 ⟨i, hx⟩⟩ in
have surjective f := λ ⟨x, hx⟩, let ⟨i, hi⟩ := mem_Union.1 hx in ⟨⟨i, x, hi⟩, rfl⟩,
mk_le_of_surjective this
70d943a
to
c386d27
Compare
Thanks for the feedback. Is |
|
TO CONTRIBUTORS:
Make sure you have:
For reviewers: code review check list