noncomputable def Partition.rep {α : Type u_1} {T : Set α} (P : Partition (Set α)) (ht : T ∈ P) : α

Noncomputably choose a representative from an equivalence class

Equations

• P.rep ht = ⋯.some

@[simp]

theorem Partition.rep_mem {α : Type u_1} {T : Set α} {P : Partition (Set α)} (ht : T ∈ P) : P.rep ht ∈ T

@[simp]

theorem Partition.rep_mem' {α : Type u_1} {T : Set α} {P : Partition (Set α)} (ht : T ∈ P) : P.rep ht ∈ P.supp

@[simp]

theorem Partition.partOf_rep {α : Type u_1} {T : Set α} {P : Partition (Set α)} (ht : T ∈ P) : P.partOf (P.rep ht) = T

theorem Partition.finite_of_finite {α : Type u_1} (P : Partition (Set α)) (hs : P.supp.Finite) : (↑P).Finite

theorem Partition.rel_iff_partOf_eq_partOf {α : Type u_1} {x y : α} (P : Partition (Set α)) (hx : x ∈ P.supp) (hy : y ∈ P.supp) : P x y ↔ P.partOf x = P.partOf y

theorem Partition.rel_iff_partOf_eq_partOf' {α : Type u_1} {x y : α} (P : Partition (Set α)) : P x y ↔ ∃ (_ : x ∈ P.supp) (_ : y ∈ P.supp), P.partOf x = P.partOf y

theorem Partition.rel_iff_forall {α : Type u_1} {x y : α} {P : Partition (Set α)} : P x y ↔ x ∈ P.supp ∧ ∀ t ∈ P, x ∈ t ↔ y ∈ t

theorem Partition.setOf_rel_self_eq {α : Type u_1} (P : Partition (Set α)) : {x : α | P x x} = P.supp

theorem Partition.rel_self_iff_mem {α : Type u_1} {x : α} {P : Partition (Set α)} : P x x ↔ x ∈ P.supp

theorem Partition.setOf_rel_eq {α : Type u_1} {x : α} {T : Set α} {P : Partition (Set α)} (ht : T ∈ P) (hx : x ∈ T) : {y : α | P x y} = T

theorem Partition.rep_rel {α : Type u_1} {x : α} {T : Set α} {P : Partition (Set α)} (ht : T ∈ P) (hx : x ∈ T) : P x (P.rep ht)

@[simp]

theorem Partition.rep_rel_self {α : Type u_1} {T : Set α} {P : Partition (Set α)} (ht : T ∈ P) : P (P.rep ht) (P.rep ht)

theorem Partition.setOf_rel_rep_eq {α : Type u_1} {T : Set α} {P : Partition (Set α)} (ht : T ∈ P) : {x : α | P (P.rep ht) x} = T

theorem Partition.setOf_rel_eq_partOf {α : Type u_1} (P : Partition (Set α)) (x : α) : {y : α | P x y} = P.partOf x

The partOf x is the set of y related to x. True even if x ∉ s, since both are ∅.

theorem Partition.setOf_rel_mem {α : Type u_1} {x : α} (P : Partition (Set α)) (hx : x ∈ P.supp) : {y : α | P x y} ∈ P

theorem Partition.discrete.rel_iff_eq_of_mem {α : Type u_1} {a b : α} {P : Partition (Set α)} (ha : a ∈ P.supp) : (Partition.discrete P.supp) a b ↔ a = b

structure Partition.RepFun {α : Type u_1} (P : Partition (Set α)) : Type u_1

• toFun : α → α
• apply_eq_self_of_notMem (a : α) : a ∉ P.supp → self.toFun a = a
• rel_apply_of_mem (a : α) : a ∈ P.supp → P a (self.toFun a)
• apply_eq_of_rel (a b : α) : P a b → self.toFun a = self.toFun b

@[instance_reducible]

instance Partition.instFunLikeRepFun {α : Type u_1} {P : Partition (Set α)} : FunLike P.RepFun α α

Equations

• Partition.instFunLikeRepFun = { coe := Partition.RepFun.toFun, coe_injective := ⋯ }

def Partition.RepFun.mk' {α : Type u_1} (P : Partition (Set α)) (f : α → α) {p : α → Prop} (hP : ∀ {x : α}, x ∈ P.supp ↔ p x) (h₁ : ∀ (a : α), ¬p a → f a = a) (h₂ : ∀ (a : α), p a → P a (f a)) (h₃ : ∀ (a b : α), P a b → f a = f b) : P.RepFun

Equations

• Partition.RepFun.mk' P f hP h₁ h₂ h₃ = { toFun := f, apply_eq_self_of_notMem := ⋯, rel_apply_of_mem := ⋯, apply_eq_of_rel := h₃ }

@[simp]

theorem Partition.RepFun.mk_apply {α : Type u_1} (P : Partition (Set α)) (f : α → α) (h₁ : ∀ a ∉ P.supp, f a = a) (h₂ : ∀ a ∈ P.supp, P a (f a)) (h₃ : ∀ (a b : α), P a b → f a = f b) (x : α) : { toFun := f, apply_eq_self_of_notMem := h₁, rel_apply_of_mem := h₂, apply_eq_of_rel := h₃ } x = f x

theorem Partition.RepFun.apply_of_notMem {α : Type u_1} {a : α} {P : Partition (Set α)} (f : P.RepFun) (ha : a ∉ P.supp) : f a = a

theorem Partition.RepFun.rel_apply {α : Type u_1} {a : α} {P : Partition (Set α)} (f : P.RepFun) (ha : a ∈ P.supp) : P a (f a)

theorem Partition.RepFun.rel_apply' {α : Type u_1} {a : α} {P : Partition (Set α)} (f : P.RepFun) {p : α → Prop} (hP : ∀ {x : α}, x ∈ P.supp ↔ p x) (ha : p a) : P a (f a)

theorem Partition.RepFun.apply_mem {α : Type u_1} {a : α} {P : Partition (Set α)} (f : P.RepFun) (ha : a ∈ P.supp) : f a ∈ P.supp

theorem Partition.RepFun.apply_mem' {α : Type u_1} {a : α} {P : Partition (Set α)} (f : P.RepFun) {p : α → Prop} (hP : ∀ {x : α}, x ∈ P.supp ↔ p x) (ha : p a) : p (f a)

theorem Partition.RepFun.image_subset_self {α : Type u_1} {P : Partition (Set α)} (f : P.RepFun) : ⇑f '' P.supp ⊆ P.supp

theorem Partition.RepFun.mapsTo {α : Type u_1} {P : Partition (Set α)} (f : P.RepFun) : Set.MapsTo (⇑f) P.supp P.supp

@[simp]

theorem Partition.RepFun.apply_mem_iff {α : Type u_1} {a : α} {P : Partition (Set α)} (f : P.RepFun) : f a ∈ P.supp ↔ a ∈ P.supp

theorem Partition.RepFun.apply_eq_apply {α : Type u_1} {a b : α} {P : Partition (Set α)} (f : P.RepFun) (hab : P a b) : f a = f b

theorem Partition.RepFun.rel_of_apply_eq_apply {α : Type u_1} {a b : α} {P : Partition (Set α)} (f : P.RepFun) (ha : a ∈ P.supp) (hab : f a = f b) : P a b

theorem Partition.RepFun.rel_of_ne_of_apply_eq_apply {α : Type u_1} {a b : α} {P : Partition (Set α)} (f : P.RepFun) (hne : a ≠ b) (hab : f a = f b) : P a b

theorem Partition.RepFun.apply_eq_apply_iff_rel {α : Type u_1} {a b : α} {P : Partition (Set α)} (f : P.RepFun) (ha : a ∈ P.supp) : f a = f b ↔ P a b

theorem Partition.RepFun.apply_eq_apply_iff_rel_of_ne {α : Type u_1} {a b : α} {P : Partition (Set α)} (f : P.RepFun) (hne : a ≠ b) : f a = f b ↔ P a b

@[simp]

theorem Partition.RepFun.idem {α : Type u_1} {P : Partition (Set α)} (f : P.RepFun) (a : α) : f (f a) = f a

theorem Partition.exists_extend_partial_repFun {α : Type u_1} (P : Partition (Set α)) {t : Set α} (f₀ : ↑t → α) (h_notMem : ∀ (x : ↑t), ↑x ∉ P.supp → f₀ x = ↑x) (h_mem : ∀ (x : ↑t), ↑x ∈ P.supp → P (↑x) (f₀ x)) (h_eq : ∀ (x y : ↑t), P ↑x ↑y → f₀ x = f₀ y) : ∃ (f : P.RepFun), ∀ (x : ↑t), f ↑x = f₀ x

Any partially defined RepFun extends to a complete one.

theorem Partition.exists_extend_partial_repFun' {α : Type u_1} (P : Partition (Set α)) {t : Set α} (h : ∀ ⦃x y : α⦄, x ∈ t → y ∈ t → P x y → x = y) : ∃ (f : P.RepFun), Set.EqOn (⇑f) id t

For any set t containining no two distinct related elements, there is a RepFun equal to the identity on t.

theorem Partition.nonempty_repFun {α : Type u_1} (P : Partition (Set α)) : Nonempty P.RepFun

@[simp]

theorem Partition.repFun_repFun {α : Type u_1} {P : Partition (Set α)} (f f' : P.RepFun) (x : α) : f (f' x) = f x

@[simp]

theorem Partition.repFun_discrete_coeFun {α : Type u_1} (s : Set α) (f : (Partition.discrete s).RepFun) : ⇑f = id

theorem Partition.RepFun.coeFun_eq_id_of_eq_discrete {α : Type u_1} {s : Set α} {P : Partition (Set α)} (f : P.RepFun) (hP : P = Partition.discrete s) : ⇑f = id

def Partition.fiber {α : Type u_1} (f : α → α) : Partition (Set α)

Equations

• Partition.fiber f = Partition.ofIndependent' ⋯

@[simp]

theorem Partition.mem_fiber_iff {α : Type u_1} {S : Set α} (f : α → α) : S ∈ fiber f ↔ (∃ (a : α), f ⁻¹' {a} = S) ∧ S ≠ ∅

@[simp]

theorem Partition.preimage_apply_mem_fiber {α : Type u_1} (f : α → α) (a : α) : f ⁻¹' {f a} ∈ fiber f

@[simp]

theorem Partition.fiber_rel_iff {α : Type u_1} {x y : α} (f : α → α) : (fiber f) x y ↔ f x = f y

theorem Partition.le_fiber_iff {α : Type u_1} {P : Partition (Set α)} (f : α → α) : P ≤ fiber f ↔ ∀ (a b : α), P a b → f a = f b

IsRepFun

structure Partition.IsRepFun {α : Type u_1} (P : Partition (Set α)) (f : α → α) : Prop

A predicate characterizing when a function f : α → α is a representative function for a partition P. A representative function maps each element to a canonical representative in its equivalence class, is the identity outside the support, and maps related elements to the same representative.

• apply_of_notMem ⦃a : α⦄ : a ∉ P.supp → f a = a
• rel_apply ⦃a : α⦄ : a ∈ P.supp → P a (f a)
• apply_eq_apply ⦃a b : α⦄ : P a b → f a = f b

theorem Partition.IsRepFun.mk' {α : Type u_1} {p : α → Prop} (P : Partition (Set α)) (f : α → α) (hP : ∀ {x : α}, x ∈ P.supp ↔ p x) (h₁ : ∀ (a : α), ¬p a → f a = a) (h₂ : ∀ (a : α), p a → P a (f a)) (h₃ : ∀ (a b : α), P a b → f a = f b) : P.IsRepFun f

Constructor for IsRepFun that uses a custom membership predicate.

theorem Partition.IsRepFun.rel_apply' {α : Type u_1} {a : α} {P : Partition (Set α)} {f : α → α} {p : α → Prop} (hf : P.IsRepFun f) (hP : ∀ {x : α}, x ∈ P.supp ↔ p x) (ha : p a) : P a (f a)

theorem Partition.IsRepFun.apply_mem {α : Type u_1} {a : α} {P : Partition (Set α)} {f : α → α} (hf : P.IsRepFun f) (ha : a ∈ P.supp) : f a ∈ P.supp

theorem Partition.IsRepFun.apply_mem' {α : Type u_1} {a : α} {P : Partition (Set α)} {f : α → α} {p : α → Prop} (hf : P.IsRepFun f) (hP : ∀ {x : α}, x ∈ P.supp ↔ p x) (ha : p a) : p (f a)

theorem Partition.IsRepFun.image_subset_supp {α : Type u_1} {P : Partition (Set α)} {f : α → α} (hf : P.IsRepFun f) : f '' P.supp ⊆ P.supp

theorem Partition.IsRepFun.image_subset {α : Type u_1} {P : Partition (Set α)} {f : α → α} {S : Set α} (hf : P.IsRepFun f) (hS : P.supp ⊆ S) : f '' S ⊆ S

theorem Partition.IsRepFun.mapsTo_supp {α : Type u_1} {P : Partition (Set α)} {f : α → α} (hf : P.IsRepFun f) : Set.MapsTo f P.supp P.supp

theorem Partition.IsRepFun.mapsTo {α : Type u_1} {P : Partition (Set α)} {f : α → α} {S : Set α} (hf : P.IsRepFun f) (hS : P.supp ⊆ S) : Set.MapsTo f S S

theorem Partition.IsRepFun.preimage_subset {α : Type u_1} {P : Partition (Set α)} {f : α → α} {S : Set α} (hf : P.IsRepFun f) (hS : P.supp ⊆ S) : f ⁻¹' S ⊆ S

theorem Partition.IsRepFun.preimage_supp_subset {α : Type u_1} {P : Partition (Set α)} {f : α → α} (hf : P.IsRepFun f) : f ⁻¹' P.supp ⊆ P.supp

@[simp]

theorem Partition.IsRepFun.apply_mem_iff {α : Type u_1} {a : α} {P : Partition (Set α)} {f : α → α} (hf : P.IsRepFun f) : f a ∈ P.supp ↔ a ∈ P.supp

theorem Partition.IsRepFun.apply_mem_iff_of_subset {α : Type u_1} {a : α} {P : Partition (Set α)} {f : α → α} {S : Set α} (hf : P.IsRepFun f) (hS : P.supp ⊆ S) : f a ∈ S ↔ a ∈ S

theorem Partition.IsRepFun.rel_of_apply_eq_apply {α : Type u_1} {a b : α} {P : Partition (Set α)} {f : α → α} (hf : P.IsRepFun f) (ha : a ∈ P.supp) (hab : f a = f b) : P a b

theorem Partition.IsRepFun.rel_of_ne_of_apply_eq_apply {α : Type u_1} {a b : α} {P : Partition (Set α)} {f : α → α} (hf : P.IsRepFun f) (hne : a ≠ b) (hab : f a = f b) : P a b

theorem Partition.IsRepFun.apply_eq_apply_iff_rel {α : Type u_1} {a b : α} {P : Partition (Set α)} {f : α → α} (hf : P.IsRepFun f) (ha : a ∈ P.supp) : f a = f b ↔ P a b

theorem Partition.IsRepFun.apply_eq_apply_iff_rel_of_ne {α : Type u_1} {a b : α} {P : Partition (Set α)} {f : α → α} (hf : P.IsRepFun f) (hne : a ≠ b) : f a = f b ↔ P a b

theorem Partition.IsRepFun.apply_eq_apply_iff {α : Type u_1} {a b : α} {P : Partition (Set α)} {f : α → α} (hf : P.IsRepFun f) : f a = f b ↔ a = b ∨ P a b

theorem Partition.IsRepFun.forall_apply_eq_apply_iff {α : Type u_1} {P : Partition (Set α)} {f : α → α} (hf : P.IsRepFun f) (a : α) : (∀ (x : α), f a = f x ↔ a = x) ∨ ∀ (x : α), f a = f x ↔ P a x

theorem Partition.IsRepFun.apply_eq_apply_iff' {α : Type u_1} {a b : α} {P : Partition (Set α)} {f : α → α} (hf : P.IsRepFun f) : f a = f b ↔ (a = b ∧ ∀ (c : α), f a = f c ↔ a = c) ∨ P a b

theorem Partition.IsRepFun.idem {α : Type u_1} {a : α} {P : Partition (Set α)} {f : α → α} (hf : P.IsRepFun f) : f (f a) = f a

theorem Partition.IsRepFun.notMem_image_supp_of_rel_of_ne_apply {α : Type u_1} {a b : α} {P : Partition (Set α)} {f : α → α} (hf : P.IsRepFun f) (hab : P a b) (h : a ≠ f b) : a ∉ f '' P.supp

theorem Partition.exists_extend_partial {α : Type u_1} (P : Partition (Set α)) {t : Set α} (f₀ : ↑t → α) (h_notMem : ∀ (x : ↑t), ↑x ∉ P.supp → f₀ x = ↑x) (h_mem : ∀ (x : ↑t), ↑x ∈ P.supp → P (↑x) (f₀ x)) (h_eq : ∀ (x y : ↑t), P ↑x ↑y → f₀ x = f₀ y) : ∃ (f : α → α), P.IsRepFun f ∧ ∀ (x : ↑t), f ↑x = f₀ x

Any partially defined representative function extends to a complete one.

theorem Partition.exists_extend_partial' {α : Type u_1} (P : Partition (Set α)) {t : Set α} (h : ∀ ⦃x y : α⦄, x ∈ t → y ∈ t → P x y → x = y) : ∃ (f : α → α), P.IsRepFun f ∧ Set.EqOn f id t

For any set t containing no two distinct related elements, there is a representative function equal to the identity on t.

theorem Partition.isRepFun_nonempty {α : Type u_1} (P : Partition (Set α)) : ∃ (f : α → α), P.IsRepFun f

theorem Partition.isRepFun_isRepFun {α : Type u_1} {P : Partition (Set α)} {f g : α → α} (hf : P.IsRepFun f) (hg : P.IsRepFun g) (x : α) : f (g x) = f x

theorem Partition.IsRepFun.eq_id_of_discrete {α : Type u_1} {f : α → α} (s : Set α) (hf : (Partition.discrete s).IsRepFun f) : f = id

theorem Partition.IsRepFun.eq_id_of_eq_discrete {α : Type u_1} {s : Set α} {P : Partition (Set α)} {f : α → α} (hf : P.IsRepFun f) (hP : P = Partition.discrete s) : f = id

def Partition.IsRepFun.toRepFun {α : Type u_1} {P : Partition (Set α)} {f : α → α} (hf : P.IsRepFun f) : P.RepFun

Convert an IsRepFun proof to a RepFun.

Equations

• hf.toRepFun = { toFun := f, apply_eq_self_of_notMem := ⋯, rel_apply_of_mem := ⋯, apply_eq_of_rel := ⋯ }

theorem Partition.RepFun.isRepFun {α : Type u_1} {P : Partition (Set α)} (rf : P.RepFun) : P.IsRepFun ⇑rf

Convert a RepFun to an IsRepFun proof.