Mathlib.Order.CompleteLattice.Finset

iSup_eq_iSup_finset theorem

(s : ι → α) : ⨆ i, s i = ⨆ t : Finset ι, ⨆ i ∈ t, s i

Full source

/-- 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 (s : ι → α) : ⨆ i, s i = ⨆ t : Finset ι, ⨆ i ∈ t, s i := by
  classical
  refine le_antisymm ?_ ?_
  · exact iSup_le fun b => le_iSup_of_le {b} <| le_iSup_of_le b <| le_iSup_of_le (by simp) <| le_rfl
  · exact iSup_le fun t => iSup_le fun b => iSup_le fun _ => le_iSup _ _

Supremum Equals Finite Suprema Supremum: $\bigsqcup_i s_i = \bigsqcup_{t \text{ finite}} \bigsqcup_{i \in t} s_i$

Informal description

For any indexed family of elements $(s_i)_{i \in \iota}$ in a complete lattice $\alpha$, the supremum of the family $\bigsqcup_{i \in \iota} s_i$ is equal to the supremum over all finite subsets $t \subseteq \iota$ of the suprema $\bigsqcup_{i \in t} s_i$.

iSup_eq_iSup_finset' theorem

(s : ι' → α) : ⨆ i, s i = ⨆ t : Finset (PLift ι'), ⨆ i ∈ t, s (PLift.down i)

Full source

/-- 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 `PLift`s. -/
theorem iSup_eq_iSup_finset' (s : ι' → α) :
    ⨆ i, s i = ⨆ t : Finset (PLift ι'), ⨆ i ∈ t, s (PLift.down i) := by
  rw [← iSup_eq_iSup_finset, ← Equiv.plift.surjective.iSup_comp]; rfl

Supremum Equals Finite Suprema Supremum via Lifting: $\bigsqcup_i s_i = \bigsqcup_{t \text{ finite}} \bigsqcup_{i \in t} s_{\mathrm{down}(i)}$

Informal description

For any indexed family of elements $(s_i)_{i \in \iota'}$ in a complete lattice $\alpha$, the supremum of the family $\bigsqcup_{i \in \iota'} s_i$ is equal to the supremum over all finite subsets $t$ of the lifted type $\mathrm{PLift}\,\iota'$ of the suprema $\bigsqcup_{i \in t} s_i$, where $i$ is first projected back to $\iota'$ via $\mathrm{PLift.down}$.

iInf_eq_iInf_finset theorem

(s : ι → α) : ⨅ i, s i = ⨅ (t : Finset ι) (i ∈ t), s i

Full source

/-- 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 (s : ι → α) : ⨅ i, s i = ⨅ (t : Finset ι) (i ∈ t), s i :=
  @iSup_eq_iSup_finset αᵒᵈ _ _ _

Infimum Equals Finite Infima Infimum: $\bigsqcap_i s_i = \bigsqcap_{t \text{ finite}} \bigsqcap_{i \in t} s_i$

Informal description

For any indexed family of elements $(s_i)_{i \in \iota}$ in a complete lattice $\alpha$, the infimum of the family $\bigsqcap_{i \in \iota} s_i$ is equal to the infimum over all finite subsets $t \subseteq \iota$ of the infima $\bigsqcap_{i \in t} s_i$.

iInf_eq_iInf_finset' theorem

(s : ι' → α) : ⨅ i, s i = ⨅ t : Finset (PLift ι'), ⨅ i ∈ t, s (PLift.down i)

Full source

/-- 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 `PLift`s. -/
theorem iInf_eq_iInf_finset' (s : ι' → α) :
    ⨅ i, s i = ⨅ t : Finset (PLift ι'), ⨅ i ∈ t, s (PLift.down i) :=
  @iSup_eq_iSup_finset' αᵒᵈ _ _ _

Infimum Equals Finite Infima Infimum via Lifting: $\bigsqcap_i s_i = \bigsqcap_{t \text{ finite}} \bigsqcap_{i \in t} s_{\mathrm{down}(i)}$

Informal description

For any indexed family of elements $(s_i)_{i \in \iota'}$ in a complete lattice $\alpha$, the infimum of the family $\bigsqcap_{i \in \iota'} s_i$ is equal to the infimum over all finite subsets $t$ of the lifted type $\mathrm{PLift}\,\iota'$ of the infima $\bigsqcap_{i \in t} s_i$, where $i$ is first projected back to $\iota'$ via $\mathrm{PLift.down}$.

Set.iUnion_eq_iUnion_finset theorem

(s : ι → Set α) : ⋃ i, s i = ⋃ t : Finset ι, ⋃ i ∈ t, s i

Full source

/-- 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 iUnion_eq_iUnion_finset (s : ι → Set α) : ⋃ i, s i = ⋃ t : Finset ι, ⋃ i ∈ t, s i :=
  iSup_eq_iSup_finset s

Union Equals Finite Unions Union: $\bigcup_i s_i = \bigcup_{t \text{ finite}} \bigcup_{i \in t} s_i$

Informal description

For any indexed family of sets $(s_i)_{i \in \iota}$ in a type $\alpha$, the union of the family $\bigcup_{i \in \iota} s_i$ is equal to the union over all finite subsets $t \subseteq \iota$ of the unions $\bigcup_{i \in t} s_i$.

Set.iUnion_eq_iUnion_finset' theorem

(s : ι' → Set α) : ⋃ i, s i = ⋃ t : Finset (PLift ι'), ⋃ i ∈ t, s (PLift.down i)

Full source

/-- 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 `PLift`s in the right hand side. -/
theorem iUnion_eq_iUnion_finset' (s : ι' → Set α) :
    ⋃ i, s i = ⋃ t : Finset (PLift ι'), ⋃ i ∈ t, s (PLift.down i) :=
  iSup_eq_iSup_finset' s

Union as Union of Finite Subunions via Lifting: $\bigcup_i s_i = \bigcup_{t \text{ finite}} \bigcup_{i \in t} s_{\mathrm{down}(i)}$

Informal description

For any indexed family of sets $(s_i)_{i \in \iota'}$ in a type $\alpha$, the union of the family $\bigcup_{i \in \iota'} s_i$ is equal to the union over all finite subsets $t$ of the lifted type $\mathrm{PLift}\,\iota'$ of the unions $\bigcup_{i \in t} s_{\mathrm{down}(i)}$, where $i$ is first projected back to $\iota'$ via $\mathrm{PLift.down}$.

Set.iInter_eq_iInter_finset theorem

(s : ι → Set α) : ⋂ i, s i = ⋂ t : Finset ι, ⋂ i ∈ t, s i

Full source

/-- 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 iInter_eq_iInter_finset (s : ι → Set α) : ⋂ i, s i = ⋂ t : Finset ι, ⋂ i ∈ t, s i :=
  iInf_eq_iInf_finset s

Intersection Equals Finite Intersections Intersection: $\bigcap_i s_i = \bigcap_{t \text{ finite}} \bigcap_{i \in t} s_i$

Informal description

For any indexed family of sets $(s_i)_{i \in \iota}$ in a type $\alpha$, the intersection of the family $\bigcap_{i \in \iota} s_i$ is equal to the intersection over all finite subsets $t \subseteq \iota$ of the intersections $\bigcap_{i \in t} s_i$.

Set.iInter_eq_iInter_finset' theorem

(s : ι' → Set α) : ⋂ i, s i = ⋂ t : Finset (PLift ι'), ⋂ i ∈ t, s (PLift.down i)

Full source

/-- 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 `PLift`s in the right
hand side. -/
theorem iInter_eq_iInter_finset' (s : ι' → Set α) :
    ⋂ i, s i = ⋂ t : Finset (PLift ι'), ⋂ i ∈ t, s (PLift.down i) :=
  iInf_eq_iInf_finset' s

Intersection as Intersection of Finite Subintersections via Lifting: $\bigcap_i s_i = \bigcap_{t \text{ finite}} \bigcap_{i \in t} s_{\mathrm{down}(i)}$

Informal description

For any indexed family of sets $(s_i)_{i \in \iota'}$ in a type $\alpha$, the intersection of the family $\bigcap_{i \in \iota'} s_i$ is equal to the intersection over all finite subsets $t$ of the lifted type $\mathrm{PLift}\,\iota'$ of the intersections $\bigcap_{i \in t} s_{\mathrm{down}(i)}$, where $i$ is first projected back to $\iota'$ via $\mathrm{PLift.down}$.

Finset.maximal_iff_forall_insert theorem

(hP : ∀ ⦃s t⦄, P t → s ⊆ t → P s) : Maximal P s ↔ P s ∧ ∀ x ∉ s, ¬P (insert x s)

Full source

theorem maximal_iff_forall_insert (hP : ∀ ⦃s t⦄, P t → s ⊆ t → P s) :
    MaximalMaximal P s ↔ P s ∧ ∀ x ∉ s, ¬ P (insert x s) := by
  simp only [Maximal, and_congr_right_iff]
  exact fun _ ↦ ⟨fun h x hxs hx ↦ hxs <| h hx (subset_insert _ _) (mem_insert_self x s),
    fun h t ht hst x hxt ↦ by_contra fun hxs ↦ h x hxs (hP ht (insert_subset hxt hst))⟩

Characterization of Maximal Finite Sets via Insertion Operation

Informal description

Let $P$ be a predicate on finite sets of type $\alpha$ that is antitone (i.e., if $P(t)$ holds and $s \subseteq t$, then $P(s)$ holds). A finite set $s$ is maximal with respect to $P$ if and only if $P(s)$ holds and for every element $x \notin s$, the predicate $P$ does not hold for the set obtained by inserting $x$ into $s$.

Finset.minimal_iff_forall_diff_singleton theorem

(hP : ∀ ⦃s t⦄, P t → t ⊆ s → P s) : Minimal P s ↔ P s ∧ ∀ x ∈ s, ¬P (s.erase x)

Full source

theorem minimal_iff_forall_diff_singleton (hP : ∀ ⦃s t⦄, P t → t ⊆ s → P s) :
    MinimalMinimal P s ↔ P s ∧ ∀ x ∈ s, ¬ P (s.erase x) where
  mp h := ⟨h.prop, fun x hxs hx ↦ by simpa using h.le_of_le hx (erase_subset _ _) hxs⟩
  mpr h := ⟨h.1, fun t ht hts x hxs ↦ by_contra fun hxt ↦
    h.2 x hxs <| hP ht (subset_erase.2 ⟨hts, hxt⟩)⟩

Characterization of Minimal Finite Sets via Removal Operation

Informal description

Let $P$ be a predicate on finite sets of type $\alpha$ that is monotone (i.e., if $P(t)$ holds and $t \subseteq s$, then $P(s)$ holds). A finite set $s$ is minimal with respect to $P$ if and only if $P(s)$ holds and for every element $x \in s$, the predicate $P$ does not hold for the set obtained by removing $x$ from $s$.

Finset.iSup_coe theorem

[SupSet β] (f : α → β) (s : Finset α) : ⨆ x ∈ (↑s : Set α), f x = ⨆ x ∈ s, f x

Full source

theorem iSup_coe [SupSet β] (f : α → β) (s : Finset α) : ⨆ x ∈ (↑s : Set α), f x = ⨆ x ∈ s, f x :=
  rfl

Equality of Suprema over Finset and its Set Coercion

Informal description

For any type $\beta$ with a supremum operation, any function $f : \alpha \to \beta$, and any finite set $s$ of elements of type $\alpha$, the supremum of $f$ over the elements of $s$ viewed as a set is equal to the supremum of $f$ over the elements of $s$ as a finset. That is, \[ \bigsqcup_{x \in (s : \text{Set } \alpha)} f(x) = \bigsqcup_{x \in s} f(x). \]

Finset.iInf_coe theorem

[InfSet β] (f : α → β) (s : Finset α) : ⨅ x ∈ (↑s : Set α), f x = ⨅ x ∈ s, f x

Full source

theorem iInf_coe [InfSet β] (f : α → β) (s : Finset α) : ⨅ x ∈ (↑s : Set α), f x = ⨅ x ∈ s, f x :=
  rfl

Equality of Infima over Finset and its Set Coercion

Informal description

For any type $\beta$ with an infimum operation, any function $f : \alpha \to \beta$, and any finite set $s$ of elements of type $\alpha$, the infimum of $f$ over the elements of $s$ viewed as a set is equal to the infimum of $f$ over the elements of $s$ as a finset. That is, \[ \bigsqcap_{x \in (s : \text{Set } \alpha)} f(x) = \bigsqcap_{x \in s} f(x). \]

Finset.iSup_singleton theorem

(a : α) (s : α → β) : ⨆ x ∈ ({ a } : Finset α), s x = s a

Full source

theorem iSup_singleton (a : α) (s : α → β) : ⨆ x ∈ ({a} : Finset α), s x = s a := by simp

Supremum over Singleton Finset Equals Function Value

Informal description

For any element $a$ of type $\alpha$ and any function $s : \alpha \to \beta$ where $\beta$ is a complete lattice, the supremum of $s$ over the singleton finset $\{a\}$ is equal to $s(a)$. That is, \[ \bigsqcup_{x \in \{a\}} s(x) = s(a). \]

Finset.iInf_singleton theorem

(a : α) (s : α → β) : ⨅ x ∈ ({ a } : Finset α), s x = s a

Full source

theorem iInf_singleton (a : α) (s : α → β) : ⨅ x ∈ ({a} : Finset α), s x = s a := by simp

Infimum over Singleton Finset Equals Function Value

Informal description

For any element $a$ of type $\alpha$ and any function $s : \alpha \to \beta$ where $\beta$ is a complete lattice, the infimum of $s$ over the singleton finset $\{a\}$ is equal to $s(a)$. That is, \[ \bigsqcap_{x \in \{a\}} s(x) = s(a). \]

Finset.iSup_option_toFinset theorem

(o : Option α) (f : α → β) : ⨆ x ∈ o.toFinset, f x = ⨆ x ∈ o, f x

Full source

theorem iSup_option_toFinset (o : Option α) (f : α → β) : ⨆ x ∈ o.toFinset, f x = ⨆ x ∈ o, f x := by
  simp

Supremum Equality for Option to Finset Conversion

Informal description

For any option type $o$ of elements in $\alpha$ and any function $f : \alpha \to \beta$ where $\beta$ is a complete lattice, the supremum of $f$ over the finset obtained from $o$ is equal to the supremum of $f$ over $o$ itself. That is, \[ \bigsqcup_{x \in \text{toFinset}(o)} f(x) = \bigsqcup_{x \in o} f(x). \]

Finset.iInf_option_toFinset theorem

(o : Option α) (f : α → β) : ⨅ x ∈ o.toFinset, f x = ⨅ x ∈ o, f x

Full source

theorem iInf_option_toFinset (o : Option α) (f : α → β) : ⨅ x ∈ o.toFinset, f x = ⨅ x ∈ o, f x :=
  @iSup_option_toFinset _ βᵒᵈ _ _ _

Infimum Equality for Option to Finset Conversion

Informal description

For any option type $o$ of elements in $\alpha$ and any function $f : \alpha \to \beta$ where $\beta$ is a complete lattice, the infimum of $f$ over the finset obtained from $o$ is equal to the infimum of $f$ over $o$ itself. That is, \[ \bigsqcap_{x \in \text{toFinset}(o)} f(x) = \bigsqcap_{x \in o} f(x). \]

Finset.iSup_union theorem

{f : α → β} {s t : Finset α} : ⨆ x ∈ s ∪ t, f x = (⨆ x ∈ s, f x) ⊔ ⨆ x ∈ t, f x

Full source

theorem iSup_union {f : α → β} {s t : Finset α} :
    ⨆ x ∈ s ∪ t, f x = (⨆ x ∈ s, f x) ⊔ ⨆ x ∈ t, f x := by simp [iSup_or, iSup_sup_eq]

Supremum over Union of Finsets Equals Join of Suprema

Informal description

For any function $f : \alpha \to \beta$ where $\beta$ is a complete lattice, and for any two finsets $s, t \subseteq \alpha$, the supremum of $f$ over the union $s \cup t$ is equal to the supremum of $f$ over $s$ joined with the supremum of $f$ over $t$. That is, \[ \bigsqcup_{x \in s \cup t} f(x) = \left(\bigsqcup_{x \in s} f(x)\right) \sqcup \left(\bigsqcup_{x \in t} f(x)\right). \]

Finset.iInf_union theorem

{f : α → β} {s t : Finset α} : ⨅ x ∈ s ∪ t, f x = (⨅ x ∈ s, f x) ⊓ ⨅ x ∈ t, f x

Full source

theorem iInf_union {f : α → β} {s t : Finset α} :
    ⨅ x ∈ s ∪ t, f x = (⨅ x ∈ s, f x) ⊓ ⨅ x ∈ t, f x :=
  @iSup_union α βᵒᵈ _ _ _ _ _

Infimum over Union of Finite Sets Equals Meet of Infima

Informal description

For any function $f \colon \alpha \to \beta$ where $\beta$ is a complete lattice, and for any two finite sets $s, t \subseteq \alpha$, the infimum of $f$ over the union $s \cup t$ is equal to the meet of the infimum of $f$ over $s$ and the infimum of $f$ over $t$. That is, \[ \bigsqcap_{x \in s \cup t} f(x) = \left(\bigsqcap_{x \in s} f(x)\right) \sqcap \left(\bigsqcap_{x \in t} f(x)\right). \]

Finset.iSup_insert theorem

(a : α) (s : Finset α) (t : α → β) : ⨆ x ∈ insert a s, t x = t a ⊔ ⨆ x ∈ s, t x

Full source

theorem iSup_insert (a : α) (s : Finset α) (t : α → β) :
    ⨆ x ∈ insert a s, t x = t a ⊔ ⨆ x ∈ s, t x := by
  rw [insert_eq]
  simp only [iSup_union, Finset.iSup_singleton]

Supremum over Inserted Finset Equals Join of Function Value and Supremum

Informal description

For any element $a$ of type $\alpha$, any finset $s \subseteq \alpha$, and any function $t : \alpha \to \beta$ where $\beta$ is a complete lattice, the supremum of $t$ over the finset obtained by inserting $a$ into $s$ is equal to the join of $t(a)$ and the supremum of $t$ over $s$. That is, \[ \bigsqcup_{x \in \text{insert } a \, s} t(x) = t(a) \sqcup \left(\bigsqcup_{x \in s} t(x)\right). \]

Finset.iInf_insert theorem

(a : α) (s : Finset α) (t : α → β) : ⨅ x ∈ insert a s, t x = t a ⊓ ⨅ x ∈ s, t x

Full source

theorem iInf_insert (a : α) (s : Finset α) (t : α → β) :
    ⨅ x ∈ insert a s, t x = t a ⊓ ⨅ x ∈ s, t x :=
  @iSup_insert α βᵒᵈ _ _ _ _ _

Infimum over Inserted Finite Set Equals Meet of Function Value and Infimum

Informal description

For any element $a$ of type $\alpha$, any finite set $s \subseteq \alpha$, and any function $t \colon \alpha \to \beta$ where $\beta$ is a complete lattice, the infimum of $t$ over the finite set obtained by inserting $a$ into $s$ is equal to the meet of $t(a)$ and the infimum of $t$ over $s$. That is, \[ \bigsqcap_{x \in \text{insert } a \, s} t(x) = t(a) \sqcap \left(\bigsqcap_{x \in s} t(x)\right). \]

Finset.iSup_finset_image theorem

{f : γ → α} {g : α → β} {s : Finset γ} : ⨆ x ∈ s.image f, g x = ⨆ y ∈ s, g (f y)

Full source

theorem iSup_finset_image {f : γ → α} {g : α → β} {s : Finset γ} :
    ⨆ x ∈ s.image f, g x = ⨆ y ∈ s, g (f y) := by rw [← iSup_coe, coe_image, iSup_image, iSup_coe]

Supremum over Image Equals Supremum of Composition over Finset

Informal description

For any function $f \colon \gamma \to \alpha$, any function $g \colon \alpha \to \beta$, and any finite set $s \subseteq \gamma$, the supremum of $g$ over the image of $s$ under $f$ is equal to the supremum of $g \circ f$ over $s$. In symbols: \[ \bigsqcup_{x \in f(s)} g(x) = \bigsqcup_{y \in s} g(f(y)). \]

Finset.iInf_finset_image theorem

{f : γ → α} {g : α → β} {s : Finset γ} : ⨅ x ∈ s.image f, g x = ⨅ y ∈ s, g (f y)

Full source

theorem iInf_finset_image {f : γ → α} {g : α → β} {s : Finset γ} :
    ⨅ x ∈ s.image f, g x = ⨅ y ∈ s, g (f y) := by rw [← iInf_coe, coe_image, iInf_image, iInf_coe]

Infimum over Finset Image Equals Infimum of Composition

Informal description

For any function $f \colon \gamma \to \alpha$, any function $g \colon \alpha \to \beta$ (where $\beta$ is a complete lattice), and any finite set $s \subseteq \gamma$, the infimum of $g$ over the image of $s$ under $f$ is equal to the infimum of $g \circ f$ over $s$. In symbols: \[ \bigsqcap_{x \in f(s)} g(x) = \bigsqcap_{y \in s} g(f(y)). \]

Finset.iSup_insert_update theorem

 {x : α} {t : Finset α} (f : α → β) {s : β} (hx : x ∉ t) : ⨆ i ∈ insert x t, Function.update f x s i = s ⊔ ⨆ i ∈ t, f i

Full source

theorem iSup_insert_update {x : α} {t : Finset α} (f : α → β) {s : β} (hx : x ∉ t) :
    ⨆ i ∈ insert x t, Function.update f x s i = s ⊔ ⨆ i ∈ t, f i := by
  simp only [Finset.iSup_insert, update_self]
  rcongr (i hi); apply update_of_ne; rintro rfl; exact hx hi

Supremum of Updated Function over Inserted Finset Equals Join of New Value and Original Supremum

Informal description

Let $\alpha$ and $\beta$ be types with $\beta$ a complete lattice. For any element $x \in \alpha$, any finite set $t \subseteq \alpha$ not containing $x$, any function $f : \alpha \to \beta$, and any element $s \in \beta$, the supremum of the updated function $\text{update } f \, x \, s$ over the set $\text{insert } x \, t$ equals the join of $s$ and the supremum of $f$ over $t$. That is, \[ \bigsqcup_{i \in \text{insert } x \, t} (\text{update } f \, x \, s)(i) = s \sqcup \left(\bigsqcup_{i \in t} f(i)\right). \]

Finset.iInf_insert_update theorem

 {x : α} {t : Finset α} (f : α → β) {s : β} (hx : x ∉ t) : ⨅ i ∈ insert x t, update f x s i = s ⊓ ⨅ i ∈ t, f i

Full source

theorem iInf_insert_update {x : α} {t : Finset α} (f : α → β) {s : β} (hx : x ∉ t) :
    ⨅ i ∈ insert x t, update f x s i = s ⊓ ⨅ i ∈ t, f i :=
  @iSup_insert_update α βᵒᵈ _ _ _ _ f _ hx

Infimum of Updated Function over Inserted Finset Equals Meet of New Value and Original Infimum

Informal description

Let $\alpha$ and $\beta$ be types with $\beta$ a complete lattice. For any element $x \in \alpha$, any finite set $t \subseteq \alpha$ not containing $x$, any function $f : \alpha \to \beta$, and any element $s \in \beta$, the infimum of the updated function $\text{update } f \, x \, s$ over the set $\text{insert } x \, t$ equals the meet of $s$ and the infimum of $f$ over $t$. That is, \[ \bigsqcap_{i \in \text{insert } x \, t} (\text{update } f \, x \, s)(i) = s \sqcap \left(\bigsqcap_{i \in t} f(i)\right). \]

Finset.iSup_biUnion theorem

(s : Finset γ) (t : γ → Finset α) (f : α → β) : ⨆ y ∈ s.biUnion t, f y = ⨆ (x ∈ s) (y ∈ t x), f y

Full source

theorem iSup_biUnion (s : Finset γ) (t : γ → Finset α) (f : α → β) :
    ⨆ y ∈ s.biUnion t, f y = ⨆ (x ∈ s) (y ∈ t x), f y := by simp [@iSup_comm _ α, iSup_and]

Supremum over Union of Finite Sets Equals Double Supremum

Informal description

For any finite set $s$ of type $\gamma$, any function $t : \gamma \to \text{Finset } \alpha$, and any function $f : \alpha \to \beta$ into a complete lattice $\beta$, the supremum of $f$ over the union of all $t(x)$ for $x \in s$ is equal to the double supremum of $f$ over all $x \in s$ and all $y \in t(x)$. In symbols: \[ \bigsqcup_{y \in \bigcup_{x \in s} t(x)} f(y) = \bigsqcup_{x \in s} \bigsqcup_{y \in t(x)} f(y). \]

Finset.iInf_biUnion theorem

(s : Finset γ) (t : γ → Finset α) (f : α → β) : ⨅ y ∈ s.biUnion t, f y = ⨅ (x ∈ s) (y ∈ t x), f y

Full source

theorem iInf_biUnion (s : Finset γ) (t : γ → Finset α) (f : α → β) :
    ⨅ y ∈ s.biUnion t, f y = ⨅ (x ∈ s) (y ∈ t x), f y :=
  @iSup_biUnion _ βᵒᵈ _ _ _ _ _ _

Infimum over Union of Finite Sets Equals Double Infimum

Informal description

For any finite set $s$ of type $\gamma$, any function $t : \gamma \to \text{Finset } \alpha$, and any function $f : \alpha \to \beta$ into a complete lattice $\beta$, the infimum of $f$ over the union of all $t(x)$ for $x \in s$ is equal to the double infimum of $f$ over all $x \in s$ and all $y \in t(x)$. In symbols: \[ \bigsqcap_{y \in \bigcup_{x \in s} t(x)} f(y) = \bigsqcap_{x \in s} \bigsqcap_{y \in t(x)} f(y). \]

Finset.set_biUnion_coe theorem

(s : Finset α) (t : α → Set β) : ⋃ x ∈ (↑s : Set α), t x = ⋃ x ∈ s, t x

Full source

theorem set_biUnion_coe (s : Finset α) (t : α → Set β) : ⋃ x ∈ (↑s : Set α), t x = ⋃ x ∈ s, t x :=
  rfl

Equality of Unions over Finite Sets and their Underlying Sets

Informal description

For any finite set $s$ of type $\alpha$ and any family of sets $t : \alpha \to \text{Set } \beta$, the union of all sets $t(x)$ for $x$ in the underlying set of $s$ is equal to the union of all sets $t(x)$ for $x$ in $s$. In symbols: \[ \bigcup_{x \in (s : \text{Set } \alpha)} t(x) = \bigcup_{x \in s} t(x). \]

Finset.set_biInter_coe theorem

(s : Finset α) (t : α → Set β) : ⋂ x ∈ (↑s : Set α), t x = ⋂ x ∈ s, t x

Full source

theorem set_biInter_coe (s : Finset α) (t : α → Set β) : ⋂ x ∈ (↑s : Set α), t x = ⋂ x ∈ s, t x :=
  rfl

Equality of Intersections over Finite Sets and their Underlying Sets

Informal description

For any finite set $s$ of type $\alpha$ and any family of sets $t : \alpha \to \text{Set } \beta$, the intersection of all sets $t(x)$ for $x$ in the underlying set of $s$ is equal to the intersection of all sets $t(x)$ for $x$ in $s$. In symbols: \[ \bigcap_{x \in (s : \text{Set } \alpha)} t(x) = \bigcap_{x \in s} t(x). \]

Finset.set_biUnion_singleton theorem

(a : α) (s : α → Set β) : ⋃ x ∈ ({ a } : Finset α), s x = s a

Full source

theorem set_biUnion_singleton (a : α) (s : α → Set β) : ⋃ x ∈ ({a} : Finset α), s x = s a :=
  iSup_singleton a s

Union over Singleton Finset Equals Function Value

Informal description

For any element $a$ of type $\alpha$ and any function $s : \alpha \to \text{Set } \beta$, the union of all sets $s(x)$ for $x$ in the singleton finset $\{a\}$ is equal to $s(a)$. That is, \[ \bigcup_{x \in \{a\}} s(x) = s(a). \]

Finset.set_biInter_singleton theorem

(a : α) (s : α → Set β) : ⋂ x ∈ ({ a } : Finset α), s x = s a

Full source

theorem set_biInter_singleton (a : α) (s : α → Set β) : ⋂ x ∈ ({a} : Finset α), s x = s a :=
  iInf_singleton a s

Intersection over Singleton Finset Equals Function Value

Informal description

For any element $a$ of type $\alpha$ and any function $s \colon \alpha \to \text{Set } \beta$, the intersection of all sets $s(x)$ for $x$ in the singleton finset $\{a\}$ is equal to $s(a)$. That is, \[ \bigcap_{x \in \{a\}} s(x) = s(a). \]

Finset.set_biUnion_preimage_singleton theorem

(f : α → β) (s : Finset β) : ⋃ y ∈ s, f ⁻¹' { y } = f ⁻¹' s

Full source

@[simp]
theorem set_biUnion_preimage_singleton (f : α → β) (s : Finset β) :
    ⋃ y ∈ s, f ⁻¹' {y} = f ⁻¹' s :=
  Set.biUnion_preimage_singleton f s

Union of Preimages of Singletons Equals Preimage of Finite Set

Informal description

For any function $f \colon \alpha \to \beta$ and any finite subset $s \subseteq \beta$, the union of the preimages of singletons $\{y\}$ for all $y \in s$ is equal to the preimage of $s$ under $f$. In symbols: $$ \bigcup_{y \in s} f^{-1}(\{y\}) = f^{-1}(s). $$

Finset.set_biUnion_option_toFinset theorem

(o : Option α) (f : α → Set β) : ⋃ x ∈ o.toFinset, f x = ⋃ x ∈ o, f x

Full source

theorem set_biUnion_option_toFinset (o : Option α) (f : α → Set β) :
    ⋃ x ∈ o.toFinset, f x = ⋃ x ∈ o, f x :=
  iSup_option_toFinset o f

Union Equality for Option to Finset Conversion

Informal description

For any option type $o$ of elements in $\alpha$ and any function $f \colon \alpha \to \text{Set } \beta$, the union of the sets $f(x)$ over the finset obtained from $o$ is equal to the union of the sets $f(x)$ over $o$ itself. That is, \[ \bigcup_{x \in \text{toFinset}(o)} f(x) = \bigcup_{x \in o} f(x). \]

Finset.set_biInter_option_toFinset theorem

(o : Option α) (f : α → Set β) : ⋂ x ∈ o.toFinset, f x = ⋂ x ∈ o, f x

Full source

theorem set_biInter_option_toFinset (o : Option α) (f : α → Set β) :
    ⋂ x ∈ o.toFinset, f x = ⋂ x ∈ o, f x :=
  iInf_option_toFinset o f

Intersection Equality for Option to Finite Set Conversion

Informal description

For any option type $o$ of elements in $\alpha$ and any function $f : \alpha \to \text{Set } \beta$, the intersection of the sets $f(x)$ over the finite set obtained from $o$ is equal to the intersection of $f(x)$ over $o$ itself. That is, \[ \bigcap_{x \in \text{toFinset}(o)} f(x) = \bigcap_{x \in o} f(x). \]

Finset.subset_set_biUnion_of_mem theorem

{s : Finset α} {f : α → Set β} {x : α} (h : x ∈ s) : f x ⊆ ⋃ y ∈ s, f y

Full source

theorem subset_set_biUnion_of_mem {s : Finset α} {f : α → Set β} {x : α} (h : x ∈ s) :
    f x ⊆ ⋃ y ∈ s, f y :=
  show f x ≤ ⨆ y ∈ s, f y from le_iSup_of_le x <| by simp only [h, iSup_pos, le_refl]

Element's Image is Subset of Finite Union: $f(x) \subseteq \bigcup_{y \in s} f(y)$ for $x \in s$

Informal description

For any finite set $s$ of elements of type $\alpha$, any function $f : \alpha \to \text{Set } \beta$, and any element $x \in s$, the set $f(x)$ is a subset of the union of all sets $f(y)$ where $y$ ranges over $s$. That is, $f(x) \subseteq \bigcup_{y \in s} f(y)$.

Finset.set_biUnion_union theorem

(s t : Finset α) (u : α → Set β) : ⋃ x ∈ s ∪ t, u x = (⋃ x ∈ s, u x) ∪ ⋃ x ∈ t, u x

Full source

theorem set_biUnion_union (s t : Finset α) (u : α → Set β) :
    ⋃ x ∈ s ∪ t, u x = (⋃ x ∈ s, u x) ∪ ⋃ x ∈ t, u x :=
  iSup_union

Union of Sets over Union of Finite Sets Equals Union of Unions

Informal description

For any finite sets $s, t \subseteq \alpha$ and any function $u : \alpha \to \text{Set } \beta$, the union of the sets $u(x)$ over $x \in s \cup t$ is equal to the union of the sets $u(x)$ over $x \in s$ combined with the union of the sets $u(x)$ over $x \in t$. That is, \[ \bigcup_{x \in s \cup t} u(x) = \left(\bigcup_{x \in s} u(x)\right) \cup \left(\bigcup_{x \in t} u(x)\right). \]

Finset.set_biInter_inter theorem

(s t : Finset α) (u : α → Set β) : ⋂ x ∈ s ∪ t, u x = (⋂ x ∈ s, u x) ∩ ⋂ x ∈ t, u x

Full source

theorem set_biInter_inter (s t : Finset α) (u : α → Set β) :
    ⋂ x ∈ s ∪ t, u x = (⋂ x ∈ s, u x) ∩ ⋂ x ∈ t, u x :=
  iInf_union

Intersection of Sets over Union of Finite Sets Equals Intersection of Intersections

Informal description

For any finite sets $s, t \subseteq \alpha$ and any function $u : \alpha \to \text{Set } \beta$, the intersection of the sets $u(x)$ over $x \in s \cup t$ is equal to the intersection of the sets $u(x)$ over $x \in s$ combined with the intersection of the sets $u(x)$ over $x \in t$. That is, \[ \bigcap_{x \in s \cup t} u(x) = \left(\bigcap_{x \in s} u(x)\right) \cap \left(\bigcap_{x \in t} u(x)\right). \]

Finset.set_biUnion_insert theorem

(a : α) (s : Finset α) (t : α → Set β) : ⋃ x ∈ insert a s, t x = t a ∪ ⋃ x ∈ s, t x

Full source

theorem set_biUnion_insert (a : α) (s : Finset α) (t : α → Set β) :
    ⋃ x ∈ insert a s, t x = t a ∪ ⋃ x ∈ s, t x :=
  iSup_insert a s t

Union over Inserted Finite Set Equals Union of Singleton and Union over Original Set

Informal description

For any element $a$ of type $\alpha$, any finite set $s \subseteq \alpha$, and any function $t : \alpha \to \mathcal{P}(\beta)$, the union of the sets $t(x)$ over the finite set obtained by inserting $a$ into $s$ is equal to the union of $t(a)$ with the union of $t(x)$ over $s$. That is, \[ \bigcup_{x \in \text{insert } a \, s} t(x) = t(a) \cup \left(\bigcup_{x \in s} t(x)\right). \]

Finset.set_biInter_insert theorem

(a : α) (s : Finset α) (t : α → Set β) : ⋂ x ∈ insert a s, t x = t a ∩ ⋂ x ∈ s, t x

Full source

theorem set_biInter_insert (a : α) (s : Finset α) (t : α → Set β) :
    ⋂ x ∈ insert a s, t x = t a ∩ ⋂ x ∈ s, t x :=
  iInf_insert a s t

Intersection over Inserted Finite Set Equals Intersection of Singleton and Intersection over Original Set

Informal description

For any element $a$ of type $\alpha$, any finite set $s \subseteq \alpha$, and any function $t \colon \alpha \to \mathcal{P}(\beta)$, the intersection of the sets $t(x)$ over the finite set obtained by inserting $a$ into $s$ is equal to the intersection of $t(a)$ with the intersection of $t(x)$ over $s$. That is, \[ \bigcap_{x \in \text{insert } a \, s} t(x) = t(a) \cap \left(\bigcap_{x \in s} t(x)\right). \]

Finset.set_biUnion_finset_image theorem

{f : γ → α} {g : α → Set β} {s : Finset γ} : ⋃ x ∈ s.image f, g x = ⋃ y ∈ s, g (f y)

Full source

theorem set_biUnion_finset_image {f : γ → α} {g : α → Set β} {s : Finset γ} :
    ⋃ x ∈ s.image f, g x = ⋃ y ∈ s, g (f y) :=
  iSup_finset_image

Union over Image Equals Union of Composition over Finite Set

Informal description

For any function $f \colon \gamma \to \alpha$, any function $g \colon \alpha \to \mathcal{P}(\beta)$, and any finite set $s \subseteq \gamma$, the union of the sets $g(x)$ over the image of $s$ under $f$ is equal to the union of $g(f(y))$ over $s$. In symbols: \[ \bigcup_{x \in f(s)} g(x) = \bigcup_{y \in s} g(f(y)). \]

Finset.set_biInter_finset_image theorem

{f : γ → α} {g : α → Set β} {s : Finset γ} : ⋂ x ∈ s.image f, g x = ⋂ y ∈ s, g (f y)

Full source

theorem set_biInter_finset_image {f : γ → α} {g : α → Set β} {s : Finset γ} :
    ⋂ x ∈ s.image f, g x = ⋂ y ∈ s, g (f y) :=
  iInf_finset_image

Intersection over Finset Image Equals Intersection of Composition over Finset

Informal description

For any function $f \colon \gamma \to \alpha$, any function $g \colon \alpha \to \mathcal{P}(\beta)$, and any finite set $s \subseteq \gamma$, the intersection of the sets $g(x)$ over the image of $s$ under $f$ is equal to the intersection of $g(f(y))$ over $s$. In symbols: \[ \bigcap_{x \in f(s)} g(x) = \bigcap_{y \in s} g(f(y)). \]

Finset.set_biUnion_insert_update theorem

 {x : α} {t : Finset α} (f : α → Set β) {s : Set β} (hx : x ∉ t) :
  ⋃ i ∈ insert x t, @update _ _ _ f x s i = s ∪ ⋃ i ∈ t, f i

Full source

theorem set_biUnion_insert_update {x : α} {t : Finset α} (f : α → Set β) {s : Set β} (hx : x ∉ t) :
    ⋃ i ∈ insert x t, @update _ _ _ f x s i = s ∪ ⋃ i ∈ t, f i :=
  iSup_insert_update f hx

Union of Updated Function over Inserted Finset Equals Union of New Set and Original Union

Informal description

Let $\alpha$ and $\beta$ be types, $x \in \alpha$ an element, $t$ a finite subset of $\alpha$ not containing $x$, $f : \alpha \to \text{Set } \beta$ a function, and $s \subseteq \beta$ a set. Then the union of the updated function $\text{update } f \, x \, s$ over the finite set $\text{insert } x \, t$ equals the union of $s$ with the union of $f$ over $t$. That is, \[ \bigcup_{i \in \text{insert } x \, t} (\text{update } f \, x \, s)(i) = s \cup \left(\bigcup_{i \in t} f(i)\right). \]

Finset.set_biInter_insert_update theorem

 {x : α} {t : Finset α} (f : α → Set β) {s : Set β} (hx : x ∉ t) :
  ⋂ i ∈ insert x t, @update _ _ _ f x s i = s ∩ ⋂ i ∈ t, f i

Full source

theorem set_biInter_insert_update {x : α} {t : Finset α} (f : α → Set β) {s : Set β} (hx : x ∉ t) :
    ⋂ i ∈ insert x t, @update _ _ _ f x s i = s ∩ ⋂ i ∈ t, f i :=
  iInf_insert_update f hx

Intersection of Updated Function over Inserted Finset Equals Intersection of New Set and Original Intersection

Informal description

Let $\alpha$ and $\beta$ be types, $x \in \alpha$ an element, $t$ a finite subset of $\alpha$ not containing $x$, $f : \alpha \to \text{Set } \beta$ a function, and $s \subseteq \beta$ a set. Then the intersection of the updated function $\text{update } f \, x \, s$ over the finite set $\text{insert } x \, t$ equals the intersection of $s$ with the intersection of $f$ over $t$. That is, \[ \bigcap_{i \in \text{insert } x \, t} (\text{update } f \, x \, s)(i) = s \cap \left(\bigcap_{i \in t} f(i)\right). \]

Finset.set_biUnion_biUnion theorem

 (s : Finset γ) (t : γ → Finset α) (f : α → Set β) : ⋃ y ∈ s.biUnion t, f y = ⋃ (x ∈ s) (y ∈ t x), f y

Full source

theorem set_biUnion_biUnion (s : Finset γ) (t : γ → Finset α) (f : α → Set β) :
    ⋃ y ∈ s.biUnion t, f y = ⋃ (x ∈ s) (y ∈ t x), f y :=
  iSup_biUnion s t f

Double Union Equality for Finite Set Unions

Informal description

For any finite set $s$ of type $\gamma$, any function $t : \gamma \to \text{Finset } \alpha$, and any function $f : \alpha \to \text{Set } \beta$, the union of the sets $f(y)$ over all $y$ in the union of $t(x)$ for $x \in s$ is equal to the double union of the sets $f(y)$ over all $x \in s$ and all $y \in t(x)$. In symbols: \[ \bigcup_{y \in \bigcup_{x \in s} t(x)} f(y) = \bigcup_{x \in s} \bigcup_{y \in t(x)} f(y). \]

Finset.set_biInter_biUnion theorem

 (s : Finset γ) (t : γ → Finset α) (f : α → Set β) : ⋂ y ∈ s.biUnion t, f y = ⋂ (x ∈ s) (y ∈ t x), f y

Full source

theorem set_biInter_biUnion (s : Finset γ) (t : γ → Finset α) (f : α → Set β) :
    ⋂ y ∈ s.biUnion t, f y = ⋂ (x ∈ s) (y ∈ t x), f y :=
  iInf_biUnion s t f

Double Intersection Equality for Finite Set Unions

Informal description

For any finite set $s$ of type $\gamma$, any function $t : \gamma \to \text{Finset } \alpha$, and any function $f : \alpha \to \text{Set } \beta$, the intersection of the sets $f(y)$ over all $y$ in the union of $t(x)$ for $x \in s$ is equal to the double intersection of the sets $f(y)$ over all $x \in s$ and all $y \in t(x)$. In symbols: \[ \bigcap_{y \in \bigcup_{x \in s} t(x)} f(y) = \bigcap_{x \in s} \bigcap_{y \in t(x)} f(y). \]