@[simp]
theorem
Finset.preimage_inter
{α : Type u}
{β : Type v}
[DecidableEq α]
[DecidableEq β]
{f : α → β}
{s t : Finset β}
(hs : Set.InjOn f (f ⁻¹' ↑s))
(ht : Set.InjOn f (f ⁻¹' ↑t))
:
@[simp]
theorem
Finset.preimage_union
{α : Type u}
{β : Type v}
[DecidableEq α]
[DecidableEq β]
{f : α → β}
{s t : Finset β}
(hst : Set.InjOn f (f ⁻¹' ↑(s ∪ t)))
:
@[simp]
theorem
Finset.preimage_compl
{α : Type u}
{β : Type v}
[DecidableEq α]
[DecidableEq β]
[Fintype α]
[Fintype β]
{f : α → β}
(s : Finset β)
(hf : Function.Injective f)
:
theorem
Finset.image_preimage_of_bij
{α : Type u}
{β : Type v}
[DecidableEq β]
(f : α → β)
(s : Finset β)
(hf : Set.BijOn f (f ⁻¹' ↑s) ↑s)
:
theorem
Finset.sigma_image_fst_preimage_mk
{α : Type u}
{β : α → Type u_1}
[DecidableEq α]
(s : Finset ((a : α) × β a))
: