noncomputable def
Set.imageSplitting
{A : Type u_1}
{B : Type u_2}
(f : A → B)
(S : Set A)
:
↑(f '' S) → ↑S
Equations
- Set.imageSplitting f S x = ⟨Classical.choose ⋯, ⋯⟩
Instances For
@[simp]
theorem
Set.imageSplitting_apply
{A : Type u_1}
{B : Type u_2}
(f : A → B)
{S : Set A}
(x : ↑(f '' S))
:
f ↑(Set.imageSplitting f S x) = ↑x
@[simp]
theorem
Set.imageSplitting_comp
{A : Type u_1}
{B : Type u_2}
(f : A → B)
(S : Set A)
:
f ∘ Subtype.val ∘ Set.imageSplitting f S = Subtype.val
@[simp]
theorem
Set.rangeSplitting_apply_coe
{A : Type u_1}
{B : Type u_2}
(f : A → B)
(inj : Function.Injective f)
(x : A)
:
Set.rangeSplitting f ⟨f x, ⋯⟩ = x