maps_to.restrict_codom

Stream: Is there code for X?

[Nicolò Cavalleri]

I know about maps_to.restrict, but is this in mathlib?

def maps_to.restrict_codom (f : α → β) (t : set β) (h : maps_to f univ t) :
  α → t := λ a, ⟨f a, h (mem_univ a)⟩

[Eric Wieser]

(docs#set.maps_to.restrict for reference)

[Nicolò Cavalleri]

I ask because there exists as well docs#set.restrict

[Eric Wieser]

docs#equiv.set.univ composed with restrict looks like it gives what you want

[Eric Wieser]

But your version reduces definitionally in a nicer way I suspect

[Nicolò Cavalleri]

It does but I was wondering if there were a direct definition with some API, as there is for set.restrict (set.restrict could also be recovered in other ways, but it still worth having it)

[Eric Wieser]

Is docs#subtype.coind close?

[Eric Wieser]

(since coe_sort s is the same as subtype (∈ s))

[Nicolò Cavalleri]

Eric Wieser said:

Is docs#subtype.coind close?

Yes!

[Nicolò Cavalleri]

#8200

[Nicolò Cavalleri]

For future reference, it turns out it already existed as docs#set.cod_restrict

[Eric Wieser]

A question for others reading this thread: Do we still want another def for convenience?

/- Alias of `set.cod_restrict` for dot notation -/
def maps_to.cod_restrict {f : α → β} {t : set β} (h : maps_to f univ t) :
  α → t := t.cod_restrict f $ (t.maps_univ_to f).mp h

If so, should it be @[simp]? abbreviation? Both?

[Nicolò Cavalleri]

In case, I propose instead that cod_restrict be refactored to this one (also, cod_restrict has a lot of unnecessary explicit parameters that should be refactored). I actually believe we should give another name to maps_to f univ, like has_image_in or set.contains_image_of, and refactor with that one.

[Eric Wieser]

Right, we already have set.range f ⊆ s as yet another spelling of maps_to f univ s, but that unfolds to ∀ ⦃x : β⦄, (∃ (y : α), f y = x) → x ∈ s which is much worse than ∀ y, f y ∈ s which is how I assume you propose we define has_image_in

[Nicolò Cavalleri]

Yes, even though the main reason why I propose has_image_in is to use dot notation. Could we use dot notation with set.range f ⊆ s?

[Nicolò Cavalleri]

Also, for personal culture, what are the parentheses ⦃ in the expression you wrote?

[Eric Wieser]

If I have h : ∀ ⦃x : β⦄, p x → β and hx : p x, then applying one to the other givesh hx : β

[Eric Wieser]

If those were {} then lean would eagerly remove x before I apply it

[Nicolò Cavalleri]

Nicolò Cavalleri said:

Yes, even though the main reason why I propose has_image_in is to use dot notation. Could we use dot notation with set.range f ⊆ s?

What about this one?

[Nicolò Cavalleri]

Eric Wieser said:

If those were {} then lean would eagerly remove x before I apply it

Thanks! I am not sure I understand what "eagerly remove x before I apply it" means but I guess I will find out when I will need to face this problem

[Hunter Monroe]

What is the current name for exists_mem_of_ne_empty which apparently says roughly `lemma nonempty_of_nonempty {α : Type*} {A : set α} : A ≠ ∅ → ∃ x, x ∈ A?