@[simp]

theorem Set.injOn_const_iff {α : Type u_1} {β : Type u_2} {s : Set α} {b : β} : InjOn (fun (x : α) => b) s ↔ s.Subsingleton

@[simp]

theorem Set.image_update {α : Type u_3} {β : Type u_4} [DecidableEq α] (a : α) (f : α → β) (s : Set α) [Decidable (a ∈ s)] (b : β) : Function.update f a b '' s = if a ∈ s then insert b (f '' (s \ {a})) else f '' s

theorem Set.preimage_update_of_notMem_notMem {α : Type u_3} {β : Type u_4} [DecidableEq α] {a : α} {b : β} (f : α → β) {s : Set β} (hbs : b ∉ s) (has : f a ∉ s) : Function.update f a b ⁻¹' s = f ⁻¹' s

theorem Set.preimage_update_of_notMem_mem {α : Type u_3} {β : Type u_4} [DecidableEq α] {a : α} {b : β} (f : α → β) {s : Set β} (hbs : b ∉ s) (has : f a ∈ s) : Function.update f a b ⁻¹' s = f ⁻¹' s \ {a}

theorem Set.preimage_update_of_mem {α : Type u_3} {β : Type u_4} [DecidableEq α] {a : α} {b : β} (f : α → β) {s : Set β} (hbs : b ∈ s) : Function.update f a b ⁻¹' s = insert a (f ⁻¹' s)

theorem Set.preimage_update_eq_ite {α : Type u_3} {β : Type u_4} [DecidableEq α] (f : α → β) (a : α) (b : β) (s : Set β) [Decidable (b ∈ s)] [Decidable (f a ∈ s)] : Function.update f a b ⁻¹' s = if b ∈ s then insert a (f ⁻¹' s) else if f a ∈ s then f ⁻¹' s \ {a} else f ⁻¹' s

theorem Set.image_update_id_apply {α : Type u_3} [DecidableEq α] (x y : α) (s : Set α) [Decidable (x ∈ s)] : Function.update id x y '' s = if x ∉ s then s else insert y (s \ {x})

theorem Set.update_injective {α : Type u_3} {β : Type u_4} [DecidableEq α] {f : α → β} {b : β} (hf : Function.Injective f) (a : α) (h : b ∉ range f) : Function.Injective (Function.update f a b)

theorem Set.update_injOn_iff {α : Type u_3} {β : Type u_4} [DecidableEq α] {f : α → β} {s : Set α} {a : α} {b : β} : InjOn (Function.update f a b) s ↔ InjOn f (s \ {a}) ∧ (a ∈ s → ∀ x ∈ s, f x = b → x = a)

@[simp]

theorem Set.update_id_injOn_iff {α : Type u_3} [DecidableEq α] {a b : α} {s : Set α} : InjOn (Function.update id a b) s ↔ a ∈ s → b ∈ s → a = b

theorem Set.BijOn.bijOn_insert_iff {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α} {t : Set β} {x : α} {y : β} (h : BijOn f s t) (hx : x ∉ s) : BijOn f (Insert.insert x s) (Insert.insert y t) ↔ y = f x ∧ y ∉ t

theorem Set.BijOn.insert_notMem {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α} {t : Set β} {x : α} (h : BijOn f s t) (hx : x ∉ s) (hx' : f x ∉ t) : BijOn f (Insert.insert x s) (Insert.insert (f x) t)

theorem Set.BijOn.diff_singleton {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α} {t : Set β} {x : α} (h : BijOn f s t) (hx : x ∈ s) : BijOn f (s \ {x}) (t \ {f x})

theorem Set.BijOn.bijOn_update {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α} {t : Set β} {x : α} {y : β} [DecidableEq α] (h : BijOn f s t) (hx : x ∈ s) (hy : y ∉ t) : BijOn (Function.update f x y) s (Insert.insert y (t \ {f x}))

@[simp]

theorem Set.injective_const_iff {α : Type u_1} {β : Type u_2} {y : β} : (Function.Injective fun (x : α) => y) ↔ Subsingleton α

@[simp]

theorem Set.domRestrict_const {α : Type u_1} {β : Type u_2} (s : Set α) (y : β) : (s.domRestrict fun (x : α) => y) = fun (x : ↑s) => y

def Set.Equiv.sumSet {α : Type u_1} {s t : Set α} [DecidablePred fun (x : α) => x ∈ s] (h : Disjoint s t) : ↑s ⊕ ↑t ≃ ↑(s ∪ t)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Set.Equiv.sumSet_symm_apply {α : Type u_1} {s t : Set α} [DecidablePred fun (x : α) => x ∈ s] (h : Disjoint s t) (x : ↑(s ∪ t)) : (sumSet h).symm x = if hx : ↑x ∈ s then Sum.inl ⟨↑x, hx⟩ else Sum.inr ⟨↑x, ⋯⟩

@[simp]

theorem Set.Equiv.sumSet_apply {α : Type u_1} {s t : Set α} [DecidablePred fun (x : α) => x ∈ s] (h : Disjoint s t) (a✝ : ↑s ⊕ ↑t) : (sumSet h) a✝ = Sum.elim (fun (x : ↑s) => ⟨↑x, ⋯⟩) (fun (x : ↑t) => ⟨↑x, ⋯⟩) a✝

@[simp]

theorem Set.Equiv.sumSet_symm_sum_elim {α : Type u_1} {β : Type u_2} {s t : Set α} [DecidablePred fun (x : α) => x ∈ s] (h : Disjoint s t) {f : α → β} {x : ↑(s ∪ t)} : Sum.elim (s.domRestrict f) (t.domRestrict f) ((sumSet h).symm x) = f ↑x

theorem Set.RightInvOn.injOn {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α} {s : Set α} (hinv : RightInvOn f g s) : InjOn f s

theorem Set.RightInvOn.injOn_image {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α} {s : Set α} (hinv : RightInvOn f g s) : InjOn g (f '' s)

theorem Set.LeftInvOn.injOn_image {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α} {t : Set β} (hinv : LeftInvOn f g t) : InjOn f (g '' t)

theorem Function.onFun_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {f : β → α} {g : γ → β} : onFun r (f ∘ g) = onFun (onFun r f) g

@[simp]

theorem Function.onFun_id {α : Type u_1} {r : α → α → Prop} : onFun r id = r

theorem Pairwise.of_refl {α : Type u_1} {ι : Type u_3} {r : α → α → Prop} {f : ι → α} [Std.Refl r] (h : Pairwise (Function.onFun r f)) (i j : ι) : r (f i) (f j)

theorem Pairwise.true_of_refl {α : Type u_1} {r : α → α → Prop} {x y : α} [Std.Refl r] (hr : Pairwise r) : r x y

theorem true_pairwise {α : Type u_1} : Pairwise ⊤

theorem Pairwise.iff_top_of_refl {α : Type u_1} {r : α → α → Prop} [Std.Refl r] : Pairwise r ↔ r = ⊤

theorem Pairwise.iff_true_of_refl {α : Type u_1} {r : α → α → Prop} [Std.Refl r] : Pairwise r ↔ ∀ (x y : α), r x y

theorem Pairwise.onFun_of_refl {α : Type u_1} {ι : Type u_3} {r : α → α → Prop} [Std.Refl r] (hr : Pairwise r) (f : ι → α) : Pairwise (Function.onFun r f)

theorem Set.pairwise_image_of_refl {α : Type u_1} {ι : Type u_3} {r : α → α → Prop} {f : ι → α} {s : Set ι} [Std.Refl r] : (f '' s).Pairwise r ↔ s.Pairwise (Function.onFun r f)

theorem Pairwise.onFun_comp_of_refl {α : Type u_1} {ι : Type u_3} {ι' : Type u_4} {r : α → α → Prop} {f : ι → α} [Std.Refl r] (hr : Pairwise (Function.onFun r f)) (g : ι' → ι) : Pairwise (Function.onFun r (f ∘ g))

instance instSymmDisjoint_matroid {α : Type u_1} [PartialOrder α] [OrderBot α] : Std.Symm Disjoint

theorem pairwiseDisjoint_pair {α : Type u_1} {ι : Type u_5} {i j : ι} {f : ι → α} [PartialOrder α] [OrderBot α] (hab : Function.onFun Disjoint f i j) : {i, j}.PairwiseDisjoint f

theorem pairwiseDisjoint_pair_iff {α : Type u_1} {ι : Type u_5} {i j : ι} {f : ι → α} [PartialOrder α] [OrderBot α] : {i, j}.PairwiseDisjoint f ↔ i = j ∨ Function.onFun Disjoint f i j

@[simp]

theorem Pairwise.const_of_refl {α : Type u_1} {ι : Type u_3} {r : α → α → Prop} [Std.Refl r] (x : α) : Pairwise (Function.onFun r fun (x_1 : ι) => x)

theorem pairwise_pair_of_symm {α : Type u_1} {r : α → α → Prop} {x y : α} [Std.Symm r] (hxy : r x y) : {x, y}.Pairwise r

theorem Set.Pairwise.range_of_injective {α : Type u_1} {ι : Type u_3} {r : α → α → Prop} {f : ι → α} (hf : Function.Injective f) : Pairwise (Function.onFun r f) ↔ (range f).Pairwise r

theorem Pairwise.restrict {α : Type u_1} {ι : Type u_3} {r : α → α → Prop} {f : ι → α} {s : Set ι} : Pairwise (Function.onFun r fun (x : ↑s) => f ↑x) ↔ s.Pairwise (Function.onFun r f)

theorem Pairwise.sum_left {ι : Type u_3} {ι' : Type u_4} {γ : Type u_5} {G : ι → γ} {H : ι' → γ} {r : γ → γ → Prop} (h : Pairwise (Function.onFun r (Sum.elim G H))) : Pairwise (Function.onFun r G)

theorem Pairwise.sum_right {ι : Type u_3} {ι' : Type u_4} {γ : Type u_5} {G : ι → γ} {H : ι' → γ} {r : γ → γ → Prop} (h : Pairwise (Function.onFun r (Sum.elim G H))) : Pairwise (Function.onFun r H)

Factorization along a surjective function

noncomputable def Function.Surjective.factor {A : Sort u_5} {B : Sort u_6} {C : Sort u_7} {f : A → B} (hf : Surjective f) (g : A → C) : B → C

Evaluate g at a chosen preimage under the surjection f. This is a factor of g exactly when g is constant on the fibers of f.

Equations

• hf.factor g = g ∘ Function.surjInv hf

theorem Function.FactorsThrough.trans {A : Sort u_5} {B : Sort u_6} {C : Sort u_7} {D : Sort u_8} {f : A → B} {g : A → C} {k : A → D} (hg : FactorsThrough g f) (hf : FactorsThrough f k) : FactorsThrough g k

Fiber containment is transitive, even when the codomains differ.

@[simp]

theorem Function.FactorsThrough.factor_apply {A : Sort u_5} {B : Sort u_6} {C : Sort u_7} {f : A → B} {g : A → C} (h : FactorsThrough g f) (hf : Surjective f) (a : A) : hf.factor g (f a) = g a

theorem Function.FactorsThrough.factor_comp {A : Sort u_5} {B : Sort u_6} {C : Sort u_7} {f : A → B} {g : A → C} (h : FactorsThrough g f) (hf : Surjective f) : hf.factor g ∘ f = g

The factor function solves the factorization equation.

theorem Function.FactorsThrough.factor_eq_iff {A : Sort u_5} {B : Sort u_6} {C : Sort u_7} {f : A → B} {g : A → C} (h : FactorsThrough g f) (hf : Surjective f) (d : B → C) : hf.factor g = d ↔ d ∘ f = g

Surjectivity makes the factorization unique.

theorem Function.FactorsThrough.range_factor {A : Sort u_5} {B : Sort u_6} {f : A → B} {C' : Type u_9} {g : A → C'} (h : FactorsThrough g f) (hf : Surjective f) : Set.range (hf.factor g) = Set.range g

A factor has exactly the same range as the original function.

theorem Function.FactorsThrough.surjective_factor_iff {A : Sort u_5} {B : Sort u_6} {C : Sort u_7} {f : A → B} {g : A → C} (h : FactorsThrough g f) (hf : Surjective f) : Surjective (hf.factor g) ↔ Surjective g

Factoring preserves surjectivity, also for Sort-valued functions.

theorem Function.FactorsThrough.injective_factor_iff {A : Sort u_5} {B : Sort u_6} {C : Sort u_7} {f : A → B} {g : A → C} (h : FactorsThrough g f) (hf : Surjective f) : Injective (hf.factor g) ↔ FactorsThrough f g

The factor is injective exactly when no additional fibers were identified.

@[simp]

theorem Function.Surjective.factor_self {A : Sort u_5} {B : Sort u_6} {f : A → B} (hf : Surjective f) : hf.factor f = id

theorem Function.FactorsThrough.factor_trans {A : Sort u_5} {B : Sort u_6} {C : Sort u_7} {D : Sort u_8} {f : A → B} {g : A → C} {k : A → D} (hk : FactorsThrough k g) (hf : Surjective f) (hgSurj : Surjective g) : hgSurj.factor k ∘ hf.factor g = hf.factor k

Factorization through an intermediate quotient agrees with direct factorization.

theorem Function.Surjective.factor_comp_eq_iff {A : Sort u_5} {B : Sort u_6} {C : Sort u_7} {f : A → B} (hf : Surjective f) (g : A → C) : hf.factor g ∘ f = g ↔ FactorsThrough g f

The constructed function solves the factorization equation exactly when g respects fibers.