Lattice operations on finsets

This file is concerned with how big lattice or set operations behave when indexed by a finset.

See also Mathlib/Data/Finset/Lattice.lean, which is concerned with folding binary lattice operations over a finset.

theorem iSup_eq_iSup_finset {α : Type u_2} {ι : Type u_5} [CompleteLattice α] (s : ι → α) : ⨆ (i : ι), s i = ⨆ (t : Finset ι), ⨆ i ∈ t, s i

Supremum of s i, i : ι, is equal to the supremum over t : Finset ι of suprema ⨆ i ∈ t, s i. This version assumes ι is a Type*. See iSup_eq_iSup_finset' for a version that works for ι : Sort*.

theorem iSup_eq_iSup_finset' {α : Type u_2} {ι' : Sort u_7} [CompleteLattice α] (s : ι' → α) : ⨆ (i : ι'), s i = ⨆ (t : Finset (PLift ι')), ⨆ i ∈ t, s i.down

Supremum of s i, i : ι, is equal to the supremum over t : Finset ι of suprema ⨆ i ∈ t, s i. This version works for ι : Sort*. See iSup_eq_iSup_finset for a version that assumes ι : Type* but has no PLifts.

theorem iInf_eq_iInf_finset {α : Type u_2} {ι : Type u_5} [CompleteLattice α] (s : ι → α) : ⨅ (i : ι), s i = ⨅ (t : Finset ι), ⨅ i ∈ t, s i

Infimum of s i, i : ι, is equal to the infimum over t : Finset ι of infima ⨅ i ∈ t, s i. This version assumes ι is a Type*. See iInf_eq_iInf_finset' for a version that works for ι : Sort*.

theorem iInf_eq_iInf_finset' {α : Type u_2} {ι' : Sort u_7} [CompleteLattice α] (s : ι' → α) : ⨅ (i : ι'), s i = ⨅ (t : Finset (PLift ι')), ⨅ i ∈ t, s i.down

Infimum of s i, i : ι, is equal to the infimum over t : Finset ι of infima ⨅ i ∈ t, s i. This version works for ι : Sort*. See iInf_eq_iInf_finset for a version that assumes ι : Type* but has no PLifts.

theorem Set.iUnion_eq_iUnion_finset {α : Type u_2} {ι : Type u_5} (s : ι → Set α) : ⋃ (i : ι), s i = ⋃ (t : Finset ι), ⋃ i ∈ t, s i

Union of an indexed family of sets s : ι → Set α is equal to the union of the unions of finite subfamilies. This version assumes ι : Type*. See also iUnion_eq_iUnion_finset' for a version that works for ι : Sort*.

theorem Set.iUnion_eq_iUnion_finset' {α : Type u_2} {ι' : Sort u_7} (s : ι' → Set α) : ⋃ (i : ι'), s i = ⋃ (t : Finset (PLift ι')), ⋃ i ∈ t, s i.down

Union of an indexed family of sets s : ι → Set α is equal to the union of the unions of finite subfamilies. This version works for ι : Sort*. See also iUnion_eq_iUnion_finset for a version that assumes ι : Type* but avoids PLifts in the right hand side.

theorem Set.iInter_eq_iInter_finset {α : Type u_2} {ι : Type u_5} (s : ι → Set α) : ⋂ (i : ι), s i = ⋂ (t : Finset ι), ⋂ i ∈ t, s i

Intersection of an indexed family of sets s : ι → Set α is equal to the intersection of the intersections of finite subfamilies. This version assumes ι : Type*. See also iInter_eq_iInter_finset' for a version that works for ι : Sort*.

theorem Set.iInter_eq_iInter_finset' {α : Type u_2} {ι' : Sort u_7} (s : ι' → Set α) : ⋂ (i : ι'), s i = ⋂ (t : Finset (PLift ι')), ⋂ i ∈ t, s i.down

Intersection of an indexed family of sets s : ι → Set α is equal to the intersection of the intersections of finite subfamilies. This version works for ι : Sort*. See also iInter_eq_iInter_finset for a version that assumes ι : Type* but avoids PLifts in the right hand side.

theorem Finset.maximal_iff_forall_insert {α : Type u_2} [DecidableEq α] {P : Finset α → Prop} {s : Finset α} (hP : ∀ ⦃s t : Finset α⦄, P t → s ⊆ t → P s) : Maximal P s ↔ P s ∧ ∀ x ∉ s, ¬P (insert x s)

theorem Finset.minimal_iff_forall_diff_singleton {α : Type u_2} [DecidableEq α] {P : Finset α → Prop} {s : Finset α} (hP : ∀ ⦃s t : Finset α⦄, P t → t ⊆ s → P s) : Minimal P s ↔ P s ∧ ∀ x ∈ s, ¬P (s.erase x)

Interaction with big lattice/set operations

theorem Finset.iSup_coe {α : Type u_2} {β : Type u_3} [SupSet β] (f : α → β) (s : Finset α) : ⨆ x ∈ ↑s, f x = ⨆ x ∈ s, f x

theorem Finset.iInf_coe {α : Type u_2} {β : Type u_3} [InfSet β] (f : α → β) (s : Finset α) : ⨅ x ∈ ↑s, f x = ⨅ x ∈ s, f x

theorem Finset.iSup_singleton {α : Type u_2} {β : Type u_3} [CompleteLattice β] (a : α) (s : α → β) : ⨆ x ∈ {a}, s x = s a

theorem Finset.iInf_singleton {α : Type u_2} {β : Type u_3} [CompleteLattice β] (a : α) (s : α → β) : ⨅ x ∈ {a}, s x = s a

theorem Finset.iSup_option_toFinset {α : Type u_2} {β : Type u_3} [CompleteLattice β] (o : Option α) (f : α → β) : ⨆ x ∈ o.toFinset, f x = ⨆ x ∈ o, f x

theorem Finset.iInf_option_toFinset {α : Type u_2} {β : Type u_3} [CompleteLattice β] (o : Option α) (f : α → β) : ⨅ x ∈ o.toFinset, f x = ⨅ x ∈ o, f x

theorem Finset.iSup_union {α : Type u_2} {β : Type u_3} [CompleteLattice β] [DecidableEq α] {f : α → β} {s t : Finset α} : ⨆ x ∈ s ∪ t, f x = (⨆ x ∈ s, f x) ⊔ ⨆ x ∈ t, f x

theorem Finset.iInf_union {α : Type u_2} {β : Type u_3} [CompleteLattice β] [DecidableEq α] {f : α → β} {s t : Finset α} : ⨅ x ∈ s ∪ t, f x = (⨅ x ∈ s, f x) ⊓ ⨅ x ∈ t, f x

theorem Finset.iSup_insert {α : Type u_2} {β : Type u_3} [CompleteLattice β] [DecidableEq α] (a : α) (s : Finset α) (t : α → β) : ⨆ x ∈ insert a s, t x = t a ⊔ ⨆ x ∈ s, t x

theorem Finset.iInf_insert {α : Type u_2} {β : Type u_3} [CompleteLattice β] [DecidableEq α] (a : α) (s : Finset α) (t : α → β) : ⨅ x ∈ insert a s, t x = t a ⊓ ⨅ x ∈ s, t x

theorem Finset.iSup_finset_image {α : Type u_2} {β : Type u_3} {γ : Type u_4} [CompleteLattice β] [DecidableEq α] {f : γ → α} {g : α → β} {s : Finset γ} : ⨆ x ∈ Finset.image f s, g x = ⨆ y ∈ s, g (f y)

theorem Finset.iInf_finset_image {α : Type u_2} {β : Type u_3} {γ : Type u_4} [CompleteLattice β] [DecidableEq α] {f : γ → α} {g : α → β} {s : Finset γ} : ⨅ x ∈ Finset.image f s, g x = ⨅ y ∈ s, g (f y)

theorem Finset.iSup_insert_update {α : Type u_2} {β : Type u_3} [CompleteLattice β] [DecidableEq α] {x : α} {t : Finset α} (f : α → β) {s : β} (hx : x ∉ t) : ⨆ i ∈ insert x t, Function.update f x s i = s ⊔ ⨆ i ∈ t, f i

theorem Finset.iInf_insert_update {α : Type u_2} {β : Type u_3} [CompleteLattice β] [DecidableEq α] {x : α} {t : Finset α} (f : α → β) {s : β} (hx : x ∉ t) : ⨅ i ∈ insert x t, Function.update f x s i = s ⊓ ⨅ i ∈ t, f i

theorem Finset.iSup_biUnion {α : Type u_2} {β : Type u_3} {γ : Type u_4} [CompleteLattice β] [DecidableEq α] (s : Finset γ) (t : γ → Finset α) (f : α → β) : ⨆ y ∈ s.biUnion t, f y = ⨆ x ∈ s, ⨆ y ∈ t x, f y

theorem Finset.iInf_biUnion {α : Type u_2} {β : Type u_3} {γ : Type u_4} [CompleteLattice β] [DecidableEq α] (s : Finset γ) (t : γ → Finset α) (f : α → β) : ⨅ y ∈ s.biUnion t, f y = ⨅ x ∈ s, ⨅ y ∈ t x, f y

theorem Finset.set_biUnion_coe {α : Type u_2} {β : Type u_3} (s : Finset α) (t : α → Set β) : ⋃ x ∈ ↑s, t x = ⋃ x ∈ s, t x

theorem Finset.set_biInter_coe {α : Type u_2} {β : Type u_3} (s : Finset α) (t : α → Set β) : ⋂ x ∈ ↑s, t x = ⋂ x ∈ s, t x

theorem Finset.set_biUnion_singleton {α : Type u_2} {β : Type u_3} (a : α) (s : α → Set β) : ⋃ x ∈ {a}, s x = s a

theorem Finset.set_biInter_singleton {α : Type u_2} {β : Type u_3} (a : α) (s : α → Set β) : ⋂ x ∈ {a}, s x = s a

@[simp]

theorem Finset.set_biUnion_preimage_singleton {α : Type u_2} {β : Type u_3} (f : α → β) (s : Finset β) : ⋃ y ∈ s, f ⁻¹' {y} = f ⁻¹' ↑s

theorem Finset.set_biUnion_option_toFinset {α : Type u_2} {β : Type u_3} (o : Option α) (f : α → Set β) : ⋃ x ∈ o.toFinset, f x = ⋃ x ∈ o, f x

theorem Finset.set_biInter_option_toFinset {α : Type u_2} {β : Type u_3} (o : Option α) (f : α → Set β) : ⋂ x ∈ o.toFinset, f x = ⋂ x ∈ o, f x

theorem Finset.subset_set_biUnion_of_mem {α : Type u_2} {β : Type u_3} {s : Finset α} {f : α → Set β} {x : α} (h : x ∈ s) : f x ⊆ ⋃ y ∈ s, f y

theorem Finset.set_biUnion_union {α : Type u_2} {β : Type u_3} [DecidableEq α] (s t : Finset α) (u : α → Set β) : ⋃ x ∈ s ∪ t, u x = (⋃ x ∈ s, u x) ∪ ⋃ x ∈ t, u x

theorem Finset.set_biInter_inter {α : Type u_2} {β : Type u_3} [DecidableEq α] (s t : Finset α) (u : α → Set β) : ⋂ x ∈ s ∪ t, u x = (⋂ x ∈ s, u x) ∩ ⋂ x ∈ t, u x

theorem Finset.set_biUnion_insert {α : Type u_2} {β : Type u_3} [DecidableEq α] (a : α) (s : Finset α) (t : α → Set β) : ⋃ x ∈ insert a s, t x = t a ∪ ⋃ x ∈ s, t x

theorem Finset.set_biInter_insert {α : Type u_2} {β : Type u_3} [DecidableEq α] (a : α) (s : Finset α) (t : α → Set β) : ⋂ x ∈ insert a s, t x = t a ∩ ⋂ x ∈ s, t x

theorem Finset.set_biUnion_finset_image {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq α] {f : γ → α} {g : α → Set β} {s : Finset γ} : ⋃ x ∈ Finset.image f s, g x = ⋃ y ∈ s, g (f y)

theorem Finset.set_biInter_finset_image {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq α] {f : γ → α} {g : α → Set β} {s : Finset γ} : ⋂ x ∈ Finset.image f s, g x = ⋂ y ∈ s, g (f y)

theorem Finset.set_biUnion_insert_update {α : Type u_2} {β : Type u_3} [DecidableEq α] {x : α} {t : Finset α} (f : α → Set β) {s : Set β} (hx : x ∉ t) : ⋃ i ∈ insert x t, Function.update f x s i = s ∪ ⋃ i ∈ t, f i

theorem Finset.set_biInter_insert_update {α : Type u_2} {β : Type u_3} [DecidableEq α] {x : α} {t : Finset α} (f : α → Set β) {s : Set β} (hx : x ∉ t) : ⋂ i ∈ insert x t, Function.update f x s i = s ∩ ⋂ i ∈ t, f i

theorem Finset.set_biUnion_biUnion {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq α] (s : Finset γ) (t : γ → Finset α) (f : α → Set β) : ⋃ y ∈ s.biUnion t, f y = ⋃ x ∈ s, ⋃ y ∈ t x, f y

theorem Finset.set_biInter_biUnion {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq α] (s : Finset γ) (t : γ → Finset α) (f : α → Set β) : ⋂ y ∈ s.biUnion t, f y = ⋂ x ∈ s, ⋂ y ∈ t x, f y