Stream: new members
Pedro Minicz (Aug 14 2020 at 16:55):
unfreezeI necessary in the following example? I'd expect
hX not to be an instance, as I specified it as an argument (
(hX : nonempty X)) not an instance (
[nonempty X] or
[hX : nonempty X]).
example (hX : nonempty X) (hY : #Y ≤ 1) : ¬ ∃ (f : X → Y) (B : set Y), f '' (f ⁻¹' B) ⊊ B := begin rintros ⟨f, A, h₁, h₂⟩, refine h₂ (le_antisymm h₁ _), intros y hy, rw cardinal.le_one_iff_subsingleton at hY, cases hY with hY, unfreezeI, cases hX with x, use x, specialize hY (f x) y, simpa [hY] end
Reid Barton (Aug 14 2020 at 16:56):
The binder type matters to your caller, not to you.
Pedro Minicz (Aug 14 2020 at 16:59):
But the type of the lemma is still
nonempty ?m_1 → _, so it doesn't seem that the argument would even be given as an instance by the user.
Reid Barton (Aug 14 2020 at 17:27):
It wouldn't, but what would happen at a hypothetical use site is not relevant to processing the definition itself.
Reid Barton (Aug 14 2020 at 17:29):
The different binder types don't make a difference for the purpose of the definition.
hX is treated as an instance because
nonempty is a class.
Pedro Minicz (Aug 14 2020 at 22:19):
Weird behavior. I'd expect my definition to specify how
hX is treated.
Last updated: May 10 2021 at 18:22 UTC