Mathlib.Data.Finset.Lattice.Basic

Finset.instUnion instance

: Union (Finset α)

Full source

/-- `s ∪ t` is the set such that `a ∈ s ∪ t` iff `a ∈ s` or `a ∈ t`. -/
instance : Union (Finset α) :=
  ⟨fun s t => ⟨_, t.2.ndunion s.1⟩⟩

Union Operation on Finite Sets

Informal description

For any type $\alpha$, the finite sets of $\alpha$ have a union operation where for any two finite sets $s$ and $t$, the union $s \cup t$ is the finite set containing all elements that are in $s$ or in $t$.

Finset.instInter instance

: Inter (Finset α)

Full source

/-- `s ∩ t` is the set such that `a ∈ s ∩ t` iff `a ∈ s` and `a ∈ t`. -/
instance : Inter (Finset α) :=
  ⟨fun s t => ⟨_, s.2.ndinter t.1⟩⟩

Intersection Operation on Finite Sets

Informal description

For any type $\alpha$, the finite sets of $\alpha$ have an intersection operation defined such that for any two finite sets $s$ and $t$, the intersection $s \cap t$ consists of all elements that are in both $s$ and $t$.

Finset.instLattice instance

: Lattice (Finset α)

Full source

instance : Lattice (Finset α) :=
  { Finset.partialOrder with
    sup := (· ∪ ·)
    sup_le := fun _ _ _ hs ht _ ha => (mem_ndunion.1 ha).elim (fun h => hs h) fun h => ht h
    le_sup_left := fun _ _ _ h => mem_ndunion.2 <| Or.inl h
    le_sup_right := fun _ _ _ h => mem_ndunion.2 <| Or.inr h
    inf := (· ∩ ·)
    le_inf := fun _ _ _ ht hu _ h => mem_ndinter.2 ⟨ht h, hu h⟩
    inf_le_left := fun _ _ _ h => (mem_ndinter.1 h).1
    inf_le_right := fun _ _ _ h => (mem_ndinter.1 h).2 }

Lattice Structure on Finite Sets

Informal description

For any type $\alpha$, the collection of finite subsets of $\alpha$ forms a lattice, where the join operation is given by union and the meet operation is given by intersection.

Finset.sup_eq_union theorem

: (Max.max : Finset α → Finset α → Finset α) = Union.union

Full source

@[simp]
theorem sup_eq_union : (Max.max : Finset α → Finset α → Finset α) = Union.union :=
  rfl

Supremum Equals Union for Finite Sets

Informal description

For any type $\alpha$, the supremum operation on finite subsets of $\alpha$ (when viewed as a join-semilattice) coincides with the union operation, i.e., $\max(s, t) = s \cup t$ for any finite sets $s, t \subseteq \alpha$.

Finset.inf_eq_inter theorem

: (Min.min : Finset α → Finset α → Finset α) = Inter.inter

Full source

@[simp]
theorem inf_eq_inter : (Min.min : Finset α → Finset α → Finset α) = Inter.inter :=
  rfl

Minimum Equals Intersection for Finite Sets

Informal description

For any type $\alpha$, the minimum operation on finite subsets of $\alpha$ (when viewed as a meet-semilattice) coincides with the intersection operation, i.e., $\min(s, t) = s \cap t$ for any finite sets $s, t \subseteq \alpha$.

Finset.union_val_nd theorem

(s t : Finset α) : (s ∪ t).1 = ndunion s.1 t.1

Full source

theorem union_val_nd (s t : Finset α) : (s ∪ t).1 = ndunion s.1 t.1 :=
  rfl

Underlying Multiset of Union Equals Nondeduplicated Union

Informal description

For any two finite sets $s$ and $t$ of type $\alpha$, the underlying multiset of their union $s \cup t$ is equal to the nondeduplicated union of the underlying multisets of $s$ and $t$.

Finset.union_val theorem

(s t : Finset α) : (s ∪ t).1 = s.1 ∪ t.1

Full source

@[simp]
theorem union_val (s t : Finset α) : (s ∪ t).1 = s.1 ∪ t.1 :=
  ndunion_eq_union s.2

Underlying Multiset of Union Equals Union of Underlying Multisets

Informal description

For any two finite sets $s$ and $t$ of type $\alpha$, the underlying multiset of their union $s \cup t$ is equal to the union of the underlying multisets of $s$ and $t$.

Finset.mem_union theorem

: a ∈ s ∪ t ↔ a ∈ s ∨ a ∈ t

Full source

@[simp]
theorem mem_union : a ∈ s ∪ ta ∈ s ∪ t ↔ a ∈ s ∨ a ∈ t :=
  mem_ndunion

Membership in Union of Finite Sets

Informal description

For any element $a$ and any finite sets $s$ and $t$ of type $\alpha$, the element $a$ belongs to the union $s \cup t$ if and only if $a$ belongs to $s$ or $a$ belongs to $t$.

Finset.mem_union_left theorem

(t : Finset α) (h : a ∈ s) : a ∈ s ∪ t

Full source

theorem mem_union_left (t : Finset α) (h : a ∈ s) : a ∈ s ∪ t :=
  mem_union.2 <| Or.inl h

Left Membership in Union of Finite Sets

Informal description

For any element $a$ and any finite sets $s$ and $t$ of type $\alpha$, if $a$ belongs to $s$, then $a$ belongs to the union $s \cup t$.

Finset.mem_union_right theorem

(s : Finset α) (h : a ∈ t) : a ∈ s ∪ t

Full source

theorem mem_union_right (s : Finset α) (h : a ∈ t) : a ∈ s ∪ t :=
  mem_union.2 <| Or.inr h

Right Membership in Union of Finite Sets

Informal description

For any element $a$ and any finite sets $s$ and $t$ of type $\alpha$, if $a$ belongs to $t$, then $a$ belongs to the union $s \cup t$.

Finset.forall_mem_union theorem

{p : α → Prop} : (∀ a ∈ s ∪ t, p a) ↔ (∀ a ∈ s, p a) ∧ ∀ a ∈ t, p a

Full source

theorem forall_mem_union {p : α → Prop} : (∀ a ∈ s ∪ t, p a) ↔ (∀ a ∈ s, p a) ∧ ∀ a ∈ t, p a :=
  ⟨fun h => ⟨fun a => h a ∘ mem_union_left _, fun b => h b ∘ mem_union_right _⟩,
   fun h _ab hab => (mem_union.mp hab).elim (h.1 _) (h.2 _)⟩

Universal Quantification over Union of Finite Sets

Informal description

For any predicate $p$ on elements of type $\alpha$ and any finite sets $s$ and $t$ of type $\alpha$, the following are equivalent: 1. For every element $a$ in the union $s \cup t$, the predicate $p(a)$ holds. 2. For every element $a$ in $s$, the predicate $p(a)$ holds, and for every element $a$ in $t$, the predicate $p(a)$ holds. In other words, $\forall a \in s \cup t, p(a) \leftrightarrow (\forall a \in s, p(a)) \land (\forall a \in t, p(a))$.

Finset.not_mem_union theorem

: a ∉ s ∪ t ↔ a ∉ s ∧ a ∉ t

Full source

theorem not_mem_union : a ∉ s ∪ ta ∉ s ∪ t ↔ a ∉ s ∧ a ∉ t := by rw [mem_union, not_or]

Non-membership in Union of Finite Sets

Informal description

For any element $a$ and any finite sets $s$ and $t$ of type $\alpha$, the element $a$ does not belong to the union $s \cup t$ if and only if $a$ does not belong to $s$ and $a$ does not belong to $t$. In other words, $a \notin s \cup t \leftrightarrow a \notin s \land a \notin t$.

Finset.coe_union theorem

(s₁ s₂ : Finset α) : ↑(s₁ ∪ s₂) = (s₁ ∪ s₂ : Set α)

Full source

@[simp, norm_cast]
theorem coe_union (s₁ s₂ : Finset α) : ↑(s₁ ∪ s₂) = (s₁ ∪ s₂ : Set α) :=
  Set.ext fun _ => mem_union

Equality of Underlying Set of Union of Finite Sets

Informal description

For any finite sets $s₁$ and $s₂$ of type $\alpha$, the underlying set of the union $s₁ ∪ s₂$ is equal to the union of the underlying sets of $s₁$ and $s₂$. In other words, $(s₁ ∪ s₂ : \text{Set } \alpha) = (s₁ : \text{Set } \alpha) ∪ (s₂ : \text{Set } \alpha)$.

Finset.union_subset theorem

(hs : s ⊆ u) : t ⊆ u → s ∪ t ⊆ u

Full source

theorem union_subset (hs : s ⊆ u) : t ⊆ u → s ∪ ts ∪ t ⊆ u :=
  sup_le <| le_iff_subset.2 hs

Union Subset Property for Finite Sets

Informal description

For any finite sets $s$, $t$, and $u$ of type $\alpha$, if $s$ is a subset of $u$ and $t$ is a subset of $u$, then the union $s \cup t$ is also a subset of $u$.

Finset.subset_union_left theorem

: s₁ ⊆ s₁ ∪ s₂

Full source

@[simp] lemma subset_union_left : s₁ ⊆ s₁ ∪ s₂ := fun _ ↦ mem_union_left _

Left Subset Property of Union in Finite Sets

Informal description

For any finite sets $s₁$ and $s₂$ of type $\alpha$, the set $s₁$ is a subset of the union $s₁ \cup s₂$.

Finset.subset_union_right theorem

: s₂ ⊆ s₁ ∪ s₂

Full source

@[simp] lemma subset_union_right : s₂ ⊆ s₁ ∪ s₂ := fun _ ↦  mem_union_right _

Right Subset Property of Union in Finite Sets

Informal description

For any finite sets $s₁$ and $s₂$ of type $\alpha$, the set $s₂$ is a subset of the union $s₁ \cup s₂$.

Finset.union_subset_union theorem

(hsu : s ⊆ u) (htv : t ⊆ v) : s ∪ t ⊆ u ∪ v

Full source

@[gcongr]
theorem union_subset_union (hsu : s ⊆ u) (htv : t ⊆ v) : s ∪ ts ∪ t ⊆ u ∪ v :=
  sup_le_sup (le_iff_subset.2 hsu) htv

Monotonicity of Union Operation: $s \subseteq u \land t \subseteq v \Rightarrow s \cup t \subseteq u \cup v$

Informal description

For any finite sets $s, t, u, v$ of type $\alpha$, if $s \subseteq u$ and $t \subseteq v$, then the union $s \cup t$ is a subset of the union $u \cup v$.

Finset.union_subset_union_left theorem

(h : s₁ ⊆ s₂) : s₁ ∪ t ⊆ s₂ ∪ t

Full source

@[gcongr]
theorem union_subset_union_left (h : s₁ ⊆ s₂) : s₁ ∪ ts₁ ∪ t ⊆ s₂ ∪ t :=
  union_subset_union h Subset.rfl

Left Monotonicity of Union Operation: $s₁ \subseteq s₂ \Rightarrow s₁ \cup t \subseteq s₂ \cup t$

Informal description

For any finite sets $s₁, s₂, t$ of type $\alpha$, if $s₁ \subseteq s₂$, then $s₁ \cup t \subseteq s₂ \cup t$.

Finset.union_subset_union_right theorem

(h : t₁ ⊆ t₂) : s ∪ t₁ ⊆ s ∪ t₂

Full source

@[gcongr]
theorem union_subset_union_right (h : t₁ ⊆ t₂) : s ∪ t₁s ∪ t₁ ⊆ s ∪ t₂ :=
  union_subset_union Subset.rfl h

Right Monotonicity of Union Operation on Finite Sets

Informal description

For any finite sets $s, t_1, t_2$ of type $\alpha$, if $t_1 \subseteq t_2$, then $s \cup t_1 \subseteq s \cup t_2$.

Finset.union_comm theorem

(s₁ s₂ : Finset α) : s₁ ∪ s₂ = s₂ ∪ s₁

Full source

theorem union_comm (s₁ s₂ : Finset α) : s₁ ∪ s₂ = s₂ ∪ s₁ := sup_comm _ _

Commutativity of Union Operation on Finite Sets

Informal description

For any two finite sets $s_1$ and $s_2$ of type $\alpha$, the union operation is commutative, i.e., $s_1 \cup s_2 = s_2 \cup s_1$.

Finset.instCommutativeUnion instance

: Std.Commutative (α := Finset α) (· ∪ ·)

Full source

instance : Std.Commutative (α := Finset α) (· ∪ ·) :=
  ⟨union_comm⟩

Commutativity of Union on Finite Sets

Informal description

The union operation $\cup$ on finite sets is commutative. That is, for any two finite sets $s_1$ and $s_2$ of type $\alpha$, we have $s_1 \cup s_2 = s_2 \cup s_1$.

Finset.union_assoc theorem

(s₁ s₂ s₃ : Finset α) : s₁ ∪ s₂ ∪ s₃ = s₁ ∪ (s₂ ∪ s₃)

Full source

@[simp]
theorem union_assoc (s₁ s₂ s₃ : Finset α) : s₁ ∪ s₂s₁ ∪ s₂ ∪ s₃ = s₁ ∪ (s₂ ∪ s₃) := sup_assoc _ _ _

Associativity of Union Operation on Finite Sets

Informal description

For any finite sets $s_1, s_2, s_3$ of type $\alpha$, the union operation is associative, i.e., $(s_1 \cup s_2) \cup s_3 = s_1 \cup (s_2 \cup s_3)$.

Finset.instAssociativeUnion instance

: Std.Associative (α := Finset α) (· ∪ ·)

Full source

instance : Std.Associative (α := Finset α) (· ∪ ·) :=
  ⟨union_assoc⟩

Associativity of Union on Finite Sets

Informal description

The union operation $\cup$ on finite sets of type $\alpha$ is associative. That is, for any finite sets $s_1, s_2, s_3$ of $\alpha$, we have $(s_1 \cup s_2) \cup s_3 = s_1 \cup (s_2 \cup s_3)$.

Finset.union_idempotent theorem

(s : Finset α) : s ∪ s = s

Full source

@[simp]
theorem union_idempotent (s : Finset α) : s ∪ s = s := sup_idem _

Idempotence of Union for Finite Sets

Informal description

For any finite set $s$ of type $\alpha$, the union of $s$ with itself equals $s$, i.e., $s \cup s = s$.

Finset.instIdempotentOpUnion instance

: Std.IdempotentOp (α := Finset α) (· ∪ ·)

Full source

instance : Std.IdempotentOp (α := Finset α) (· ∪ ·) :=
  ⟨union_idempotent⟩

Idempotence of Union Operation on Finite Sets

Informal description

The union operation $\cup$ on finite sets of type $\alpha$ is idempotent, meaning that for any finite set $s$, we have $s \cup s = s$.

Finset.union_subset_left theorem

(h : s ∪ t ⊆ u) : s ⊆ u

Full source

theorem union_subset_left (h : s ∪ ts ∪ t ⊆ u) : s ⊆ u :=
  subset_union_left.trans h

Left Subset Property of Union in Finite Sets

Informal description

For any finite sets $s$, $t$, and $u$ of type $\alpha$, if the union $s \cup t$ is a subset of $u$, then $s$ is a subset of $u$.

Finset.union_subset_right theorem

{s t u : Finset α} (h : s ∪ t ⊆ u) : t ⊆ u

Full source

theorem union_subset_right {s t u : Finset α} (h : s ∪ ts ∪ t ⊆ u) : t ⊆ u :=
  Subset.trans subset_union_right h

Right Subset Property of Union in Finite Sets

Informal description

For any finite sets $s$, $t$, and $u$ of type $\alpha$, if the union $s \cup t$ is a subset of $u$, then $t$ is a subset of $u$.

Finset.union_left_comm theorem

(s t u : Finset α) : s ∪ (t ∪ u) = t ∪ (s ∪ u)

Full source

theorem union_left_comm (s t u : Finset α) : s ∪ (t ∪ u) = t ∪ (s ∪ u) :=
  ext fun _ => by simp only [mem_union, or_left_comm]

Left Commutativity of Union for Finite Sets

Informal description

For any finite sets $s$, $t$, and $u$ of type $\alpha$, the union operation satisfies the left-commutativity property: $$s \cup (t \cup u) = t \cup (s \cup u).$$

Finset.union_right_comm theorem

(s t u : Finset α) : s ∪ t ∪ u = s ∪ u ∪ t

Full source

theorem union_right_comm (s t u : Finset α) : s ∪ ts ∪ t ∪ u = s ∪ us ∪ u ∪ t :=
  ext fun x => by simp only [mem_union, or_assoc, @or_comm (x ∈ t)]

Right Commutativity of Union for Finite Sets

Informal description

For any finite sets $s$, $t$, and $u$ of type $\alpha$, the union operation satisfies the right commutativity property: $(s \cup t) \cup u = (s \cup u) \cup t$.

Finset.union_self theorem

(s : Finset α) : s ∪ s = s

Full source

theorem union_self (s : Finset α) : s ∪ s = s :=
  union_idempotent s

Idempotence of Union for Finite Sets

Informal description

For any finite set $s$ of type $\alpha$, the union of $s$ with itself equals $s$, i.e., $s \cup s = s$.

Finset.union_eq_left theorem

: s ∪ t = s ↔ t ⊆ s

Full source

@[simp] lemma union_eq_left : s ∪ ts ∪ t = s ↔ t ⊆ s := sup_eq_left

Union Equals Left Operand iff Right Operand is Subset

Informal description

For any finite sets $s$ and $t$ of type $\alpha$, the union $s \cup t$ equals $s$ if and only if $t$ is a subset of $s$.

Finset.left_eq_union theorem

: s = s ∪ t ↔ t ⊆ s

Full source

@[simp] lemma left_eq_union : s = s ∪ t ↔ t ⊆ s := by rw [eq_comm, union_eq_left]

Left Set Equals Union iff Right Set is Subset

Informal description

For any finite sets $s$ and $t$ of a type $\alpha$, the equality $s = s \cup t$ holds if and only if $t$ is a subset of $s$.

Finset.union_eq_right theorem

: s ∪ t = t ↔ s ⊆ t

Full source

@[simp] lemma union_eq_right : s ∪ ts ∪ t = t ↔ s ⊆ t := sup_eq_right

Union Equals Right Operand iff Left Operand is Subset

Informal description

For any finite sets $s$ and $t$ of a type $\alpha$, the union $s \cup t$ equals $t$ if and only if $s$ is a subset of $t$.

Finset.right_eq_union theorem

: s = t ∪ s ↔ t ⊆ s

Full source

@[simp] lemma right_eq_union : s = t ∪ s ↔ t ⊆ s := by rw [eq_comm, union_eq_right]

Right Set Equals Union iff Left Set is Subset

Informal description

For any finite sets $s$ and $t$ of a type $\alpha$, the equality $s = t \cup s$ holds if and only if $t$ is a subset of $s$.

Finset.union_congr_left theorem

(ht : t ⊆ s ∪ u) (hu : u ⊆ s ∪ t) : s ∪ t = s ∪ u

Full source

theorem union_congr_left (ht : t ⊆ s ∪ u) (hu : u ⊆ s ∪ t) : s ∪ t = s ∪ u :=
  sup_congr_left ht hu

Union Congruence under Left Absorption Conditions

Informal description

For any finite sets $s$, $t$, and $u$ of a type $\alpha$, if $t \subseteq s \cup u$ and $u \subseteq s \cup t$, then $s \cup t = s \cup u$.

Finset.union_congr_right theorem

(hs : s ⊆ t ∪ u) (ht : t ⊆ s ∪ u) : s ∪ u = t ∪ u

Full source

theorem union_congr_right (hs : s ⊆ t ∪ u) (ht : t ⊆ s ∪ u) : s ∪ u = t ∪ u :=
  sup_congr_right hs ht

Union Congruence under Absorption Conditions: $s \cup u = t \cup u$

Informal description

For any finite sets $s$, $t$, and $u$ of type $\alpha$, if $s \subseteq t \cup u$ and $t \subseteq s \cup u$, then $s \cup u = t \cup u$.

Finset.union_eq_union_iff_left theorem

: s ∪ t = s ∪ u ↔ t ⊆ s ∪ u ∧ u ⊆ s ∪ t

Full source

theorem union_eq_union_iff_left : s ∪ ts ∪ t = s ∪ u ↔ t ⊆ s ∪ u ∧ u ⊆ s ∪ t :=
  sup_eq_sup_iff_left

Union Equality Criterion via Left Absorption

Informal description

For any finite sets $s$, $t$, and $u$ of a type $\alpha$, the equality $s \cup t = s \cup u$ holds if and only if $t \subseteq s \cup u$ and $u \subseteq s \cup t$.

Finset.union_eq_union_iff_right theorem

: s ∪ u = t ∪ u ↔ s ⊆ t ∪ u ∧ t ⊆ s ∪ u

Full source

theorem union_eq_union_iff_right : s ∪ us ∪ u = t ∪ u ↔ s ⊆ t ∪ u ∧ t ⊆ s ∪ u :=
  sup_eq_sup_iff_right

Union Equality Criterion via Absorption Conditions: $s \cup u = t \cup u$

Informal description

For any finite sets $s$, $t$, and $u$ of a type $\alpha$, the equality $s \cup u = t \cup u$ holds if and only if $s$ is contained in $t \cup u$ and $t$ is contained in $s \cup u$.

Finset.inter_val_nd theorem

(s₁ s₂ : Finset α) : (s₁ ∩ s₂).1 = ndinter s₁.1 s₂.1

Full source

theorem inter_val_nd (s₁ s₂ : Finset α) : (s₁ ∩ s₂).1 = ndinter s₁.1 s₂.1 :=
  rfl

Underlying List of Finite Set Intersection via `ndinter`

Informal description

For any two finite sets $s₁$ and $s₂$ of type $\alpha$, the underlying list of their intersection $s₁ ∩ s₂$ is equal to the list obtained by applying the `ndinter` function to the underlying lists of $s₁$ and $s₂$.

Finset.inter_val theorem

(s₁ s₂ : Finset α) : (s₁ ∩ s₂).1 = s₁.1 ∩ s₂.1

Full source

@[simp]
theorem inter_val (s₁ s₂ : Finset α) : (s₁ ∩ s₂).1 = s₁.1 ∩ s₂.1 :=
  ndinter_eq_inter s₁.2

Underlying Multiset of Finite Set Intersection Equals Multiset Intersection

Informal description

For any two finite sets $s_1$ and $s_2$ of elements of type $\alpha$, the underlying multiset of their intersection $s_1 \cap s_2$ is equal to the intersection of the underlying multisets of $s_1$ and $s_2$.

Finset.mem_inter theorem

{a : α} {s₁ s₂ : Finset α} : a ∈ s₁ ∩ s₂ ↔ a ∈ s₁ ∧ a ∈ s₂

Full source

@[simp]
theorem mem_inter {a : α} {s₁ s₂ : Finset α} : a ∈ s₁ ∩ s₂a ∈ s₁ ∩ s₂ ↔ a ∈ s₁ ∧ a ∈ s₂ :=
  mem_ndinter

Membership in Finite Set Intersection: $a \in s_1 \cap s_2 \leftrightarrow a \in s_1 \land a \in s_2$

Informal description

For any element $a$ of type $\alpha$ and any two finite sets $s_1$ and $s_2$ of elements of $\alpha$, the element $a$ belongs to the intersection $s_1 \cap s_2$ if and only if $a$ belongs to both $s_1$ and $s_2$.

Finset.mem_of_mem_inter_left theorem

{a : α} {s₁ s₂ : Finset α} (h : a ∈ s₁ ∩ s₂) : a ∈ s₁

Full source

theorem mem_of_mem_inter_left {a : α} {s₁ s₂ : Finset α} (h : a ∈ s₁ ∩ s₂) : a ∈ s₁ :=
  (mem_inter.1 h).1

Membership in Left Component of Finite Set Intersection

Informal description

For any element $a$ of type $\alpha$ and any two finite sets $s_1$ and $s_2$ of elements of $\alpha$, if $a$ belongs to the intersection $s_1 \cap s_2$, then $a$ belongs to $s_1$.

Finset.mem_of_mem_inter_right theorem

{a : α} {s₁ s₂ : Finset α} (h : a ∈ s₁ ∩ s₂) : a ∈ s₂

Full source

theorem mem_of_mem_inter_right {a : α} {s₁ s₂ : Finset α} (h : a ∈ s₁ ∩ s₂) : a ∈ s₂ :=
  (mem_inter.1 h).2

Membership in Right Component of Finite Set Intersection

Informal description

For any element $a$ of type $\alpha$ and any two finite sets $s_1$ and $s_2$ of elements of $\alpha$, if $a$ belongs to the intersection $s_1 \cap s_2$, then $a$ belongs to $s_2$.

Finset.mem_inter_of_mem theorem

{a : α} {s₁ s₂ : Finset α} : a ∈ s₁ → a ∈ s₂ → a ∈ s₁ ∩ s₂

Full source

theorem mem_inter_of_mem {a : α} {s₁ s₂ : Finset α} : a ∈ s₁ → a ∈ s₂ → a ∈ s₁ ∩ s₂ :=
  and_imp.1 mem_inter.2

Membership in Intersection via Membership in Both Sets

Informal description

For any element $a$ of type $\alpha$ and any two finite sets $s_1$ and $s_2$ of elements of $\alpha$, if $a$ belongs to $s_1$ and $a$ belongs to $s_2$, then $a$ belongs to the intersection $s_1 \cap s_2$.

Finset.inter_subset_left theorem

: s₁ ∩ s₂ ⊆ s₁

Full source

@[simp] lemma inter_subset_left : s₁ ∩ s₂s₁ ∩ s₂ ⊆ s₁ := fun _ ↦ mem_of_mem_inter_left

Intersection is Subset of Left Operand

Informal description

For any two finite sets $s_1$ and $s_2$ of elements of type $\alpha$, the intersection $s_1 \cap s_2$ is a subset of $s_1$.

Finset.inter_subset_right theorem

: s₁ ∩ s₂ ⊆ s₂

Full source

@[simp] lemma inter_subset_right : s₁ ∩ s₂s₁ ∩ s₂ ⊆ s₂ := fun _ ↦ mem_of_mem_inter_right

Intersection is Subset of Right Operand

Informal description

For any two finite sets $s_1$ and $s_2$ of elements of type $\alpha$, the intersection $s_1 \cap s_2$ is a subset of $s_2$.

Finset.subset_inter theorem

{s₁ s₂ u : Finset α} : s₁ ⊆ s₂ → s₁ ⊆ u → s₁ ⊆ s₂ ∩ u

Full source

theorem subset_inter {s₁ s₂ u : Finset α} : s₁ ⊆ s₂ → s₁ ⊆ u → s₁ ⊆ s₂ ∩ u := by
  simp +contextual [subset_iff, mem_inter]

Subset of Intersection via Subset of Both Sets

Informal description

For any finite sets $s₁$, $s₂$, and $u$ of type $\alpha$, if $s₁$ is a subset of $s₂$ and $s₁$ is a subset of $u$, then $s₁$ is a subset of the intersection $s₂ \cap u$.

Finset.coe_inter theorem

(s₁ s₂ : Finset α) : ↑(s₁ ∩ s₂) = (s₁ ∩ s₂ : Set α)

Full source

@[simp, norm_cast]
theorem coe_inter (s₁ s₂ : Finset α) : ↑(s₁ ∩ s₂) = (s₁ ∩ s₂ : Set α) :=
  Set.ext fun _ => mem_inter

Equality of Finite Set Intersection and Underlying Set Intersection: $(s_1 \cap s_2) = (s_1 \cap s_2)$

Informal description

For any two finite sets $s_1$ and $s_2$ of elements of type $\alpha$, the underlying set of their intersection $s_1 \cap s_2$ is equal to the intersection of their underlying sets, i.e., $(s_1 \cap s_2) = (s_1 \cap s_2)$ as sets.

Finset.union_inter_cancel_left theorem

{s t : Finset α} : (s ∪ t) ∩ s = s

Full source

@[simp]
theorem union_inter_cancel_left {s t : Finset α} : (s ∪ t) ∩ s = s := by
  rw [← coe_inj, coe_inter, coe_union, Set.union_inter_cancel_left]

Absorption Law for Union and Intersection in Finite Sets (Left Variant)

Informal description

For any finite sets $s$ and $t$ of elements of type $\alpha$, the intersection of the union $s \cup t$ with $s$ equals $s$, i.e., $(s \cup t) \cap s = s$.

Finset.union_inter_cancel_right theorem

{s t : Finset α} : (s ∪ t) ∩ t = t

Full source

@[simp]
theorem union_inter_cancel_right {s t : Finset α} : (s ∪ t) ∩ t = t := by
  rw [← coe_inj, coe_inter, coe_union, Set.union_inter_cancel_right]

Absorption Law for Union and Intersection of Finite Sets (Right Variant)

Informal description

For any finite sets $s$ and $t$ of elements of type $\alpha$, the intersection of the union $s \cup t$ with $t$ equals $t$, i.e., $(s \cup t) \cap t = t$.

Finset.inter_comm theorem

(s₁ s₂ : Finset α) : s₁ ∩ s₂ = s₂ ∩ s₁

Full source

theorem inter_comm (s₁ s₂ : Finset α) : s₁ ∩ s₂ = s₂ ∩ s₁ :=
  ext fun _ => by simp only [mem_inter, and_comm]

Commutativity of Intersection for Finite Sets

Informal description

For any two finite sets $s_1$ and $s_2$ of elements of type $\alpha$, the intersection $s_1 \cap s_2$ is equal to $s_2 \cap s_1$.

Finset.inter_assoc theorem

(s₁ s₂ s₃ : Finset α) : s₁ ∩ s₂ ∩ s₃ = s₁ ∩ (s₂ ∩ s₃)

Full source

@[simp]
theorem inter_assoc (s₁ s₂ s₃ : Finset α) : s₁ ∩ s₂s₁ ∩ s₂ ∩ s₃ = s₁ ∩ (s₂ ∩ s₃) :=
  ext fun _ => by simp only [mem_inter, and_assoc]

Associativity of Intersection for Finite Sets

Informal description

For any finite sets $s_1, s_2, s_3$ of type $\alpha$, the intersection operation is associative, i.e., $(s_1 \cap s_2) \cap s_3 = s_1 \cap (s_2 \cap s_3)$.

Finset.inter_left_comm theorem

(s₁ s₂ s₃ : Finset α) : s₁ ∩ (s₂ ∩ s₃) = s₂ ∩ (s₁ ∩ s₃)

Full source

theorem inter_left_comm (s₁ s₂ s₃ : Finset α) : s₁ ∩ (s₂ ∩ s₃) = s₂ ∩ (s₁ ∩ s₃) :=
  ext fun _ => by simp only [mem_inter, and_left_comm]

Left Commutativity of Finite Set Intersection

Informal description

For any finite sets $s_1, s_2, s_3$ of type $\alpha$, the following equality holds: $s_1 \cap (s_2 \cap s_3) = s_2 \cap (s_1 \cap s_3)$.

Finset.inter_right_comm theorem

(s₁ s₂ s₃ : Finset α) : s₁ ∩ s₂ ∩ s₃ = s₁ ∩ s₃ ∩ s₂

Full source

theorem inter_right_comm (s₁ s₂ s₃ : Finset α) : s₁ ∩ s₂s₁ ∩ s₂ ∩ s₃ = s₁ ∩ s₃s₁ ∩ s₃ ∩ s₂ :=
  ext fun _ => by simp only [mem_inter, and_right_comm]

Right Commutativity of Finite Set Intersection

Informal description

For any finite sets $s_1, s_2, s_3$ of type $\alpha$, the intersection operation is right-commutative, i.e., $(s_1 \cap s_2) \cap s_3 = (s_1 \cap s_3) \cap s_2$.

Finset.inter_self theorem

(s : Finset α) : s ∩ s = s

Full source

@[simp]
theorem inter_self (s : Finset α) : s ∩ s = s :=
  ext fun _ => mem_inter.trans <| and_self_iff

Idempotence of Finite Set Intersection: $s \cap s = s$

Informal description

For any finite set $s$ of elements of type $\alpha$, the intersection of $s$ with itself equals $s$, i.e., $s \cap s = s$.

Finset.inter_union_self theorem

(s t : Finset α) : s ∩ (t ∪ s) = s

Full source

@[simp]
theorem inter_union_self (s t : Finset α) : s ∩ (t ∪ s) = s := by
  rw [inter_comm, union_inter_cancel_right]

Absorption Law for Intersection and Union of Finite Sets: $s \cap (t \cup s) = s$

Informal description

For any finite sets $s$ and $t$ of elements of type $\alpha$, the intersection of $s$ with the union of $t$ and $s$ equals $s$, i.e., $s \cap (t \cup s) = s$.

Finset.inter_subset_inter theorem

{x y s t : Finset α} (h : x ⊆ y) (h' : s ⊆ t) : x ∩ s ⊆ y ∩ t

Full source

@[mono, gcongr]
theorem inter_subset_inter {x y s t : Finset α} (h : x ⊆ y) (h' : s ⊆ t) : x ∩ sx ∩ s ⊆ y ∩ t := by
  intro a a_in
  rw [Finset.mem_inter] at a_in ⊢
  exact ⟨h a_in.1, h' a_in.2⟩

Monotonicity of Finite Set Intersection with Respect to Subset Inclusion

Informal description

For any finite sets $x, y, s, t$ of elements of type $\alpha$, if $x \subseteq y$ and $s \subseteq t$, then $x \cap s \subseteq y \cap t$.

Finset.inter_subset_inter_left theorem

(h : t ⊆ u) : s ∩ t ⊆ s ∩ u

Full source

@[gcongr]
theorem inter_subset_inter_left (h : t ⊆ u) : s ∩ ts ∩ t ⊆ s ∩ u :=
  inter_subset_inter Subset.rfl h

Left Monotonicity of Finite Set Intersection with Respect to Subset Inclusion

Informal description

For any finite sets $s, t, u$ of elements of type $\alpha$, if $t \subseteq u$, then $s \cap t \subseteq s \cap u$.

Finset.inter_subset_inter_right theorem

(h : s ⊆ t) : s ∩ u ⊆ t ∩ u

Full source

@[gcongr]
theorem inter_subset_inter_right (h : s ⊆ t) : s ∩ us ∩ u ⊆ t ∩ u :=
  inter_subset_inter h Subset.rfl

Right Monotonicity of Finite Set Intersection with Respect to Subset Inclusion

Informal description

For any finite sets $s, t, u$ of elements of type $\alpha$, if $s \subseteq t$, then $s \cap u \subseteq t \cap u$.

Finset.inter_subset_union theorem

: s ∩ t ⊆ s ∪ t

Full source

theorem inter_subset_union : s ∩ ts ∩ t ⊆ s ∪ t :=
  le_iff_subset.1 inf_le_sup

Intersection is Subset of Union for Finite Sets

Informal description

For any two finite sets $s$ and $t$ of elements of type $\alpha$, the intersection $s \cap t$ is a subset of the union $s \cup t$.

Finset.instDistribLattice instance

: DistribLattice (Finset α)

Full source

instance : DistribLattice (Finset α) :=
  { le_sup_inf := fun a b c => by
      simp +contextual only
        [sup_eq_union, inf_eq_inter, le_eq_subset, subset_iff, mem_inter, mem_union, and_imp,
        or_imp, true_or, imp_true_iff, true_and, or_true] }

Distributive Lattice Structure on Finite Sets

Informal description

For any type $\alpha$, the collection of finite subsets of $\alpha$ forms a distributive lattice, where the join operation is given by union and the meet operation is given by intersection.

Finset.union_left_idem theorem

(s t : Finset α) : s ∪ (s ∪ t) = s ∪ t

Full source

@[simp]
theorem union_left_idem (s t : Finset α) : s ∪ (s ∪ t) = s ∪ t := sup_left_idem _ _

Left Idempotency of Union Operation on Finite Sets

Informal description

For any finite sets $s$ and $t$ of a type $\alpha$, the union operation satisfies $s \cup (s \cup t) = s \cup t$.

Finset.union_right_idem theorem

(s t : Finset α) : s ∪ t ∪ t = s ∪ t

Full source

theorem union_right_idem (s t : Finset α) : s ∪ ts ∪ t ∪ t = s ∪ t := sup_right_idem _ _

Right Idempotency of Union Operation on Finite Sets

Informal description

For any finite sets $s$ and $t$ of type $\alpha$, the union operation satisfies $(s \cup t) \cup t = s \cup t$.

Finset.inter_left_idem theorem

(s t : Finset α) : s ∩ (s ∩ t) = s ∩ t

Full source

@[simp]
theorem inter_left_idem (s t : Finset α) : s ∩ (s ∩ t) = s ∩ t := inf_left_idem _ _

Left Idempotency of Intersection Operation on Finite Sets

Informal description

For any finite sets $s$ and $t$ of a type $\alpha$, the intersection operation satisfies $s \cap (s \cap t) = s \cap t$.

Finset.inter_right_idem theorem

(s t : Finset α) : s ∩ t ∩ t = s ∩ t

Full source

theorem inter_right_idem (s t : Finset α) : s ∩ ts ∩ t ∩ t = s ∩ t := inf_right_idem _ _

Right Idempotency of Intersection on Finite Sets

Informal description

For any finite sets $s$ and $t$ of type $\alpha$, the intersection operation satisfies $(s \cap t) \cap t = s \cap t$.

Finset.inter_union_distrib_left theorem

(s t u : Finset α) : s ∩ (t ∪ u) = s ∩ t ∪ s ∩ u

Full source

theorem inter_union_distrib_left (s t u : Finset α) : s ∩ (t ∪ u) = s ∩ ts ∩ t ∪ s ∩ u :=
  inf_sup_left _ _ _

Left Distributivity of Intersection over Union in Finite Sets: $s \cap (t \cup u) = (s \cap t) \cup (s \cap u)$

Informal description

For any finite sets $s, t, u$ of a type $\alpha$, the intersection operation distributes over the union operation on the left: $$ s \cap (t \cup u) = (s \cap t) \cup (s \cap u). $$

Finset.union_inter_distrib_right theorem

(s t u : Finset α) : (s ∪ t) ∩ u = s ∩ u ∪ t ∩ u

Full source

theorem union_inter_distrib_right (s t u : Finset α) : (s ∪ t) ∩ u = s ∩ us ∩ u ∪ t ∩ u :=
  inf_sup_right _ _ _

Right Distributivity of Intersection over Union in Finite Sets: $(s \cup t) \cap u = (s \cap u) \cup (t \cap u)$

Informal description

For any finite sets $s, t, u$ of a type $\alpha$, the intersection operation distributes over the union operation on the right: $$ (s \cup t) \cap u = (s \cap u) \cup (t \cap u). $$

Finset.union_inter_distrib_left theorem

(s t u : Finset α) : s ∪ t ∩ u = (s ∪ t) ∩ (s ∪ u)

Full source

theorem union_inter_distrib_left (s t u : Finset α) : s ∪ t ∩ u = (s ∪ t) ∩ (s ∪ u) :=
  sup_inf_left _ _ _

Left Distributivity of Union over Intersection in Finite Sets: $s \cup (t \cap u) = (s \cup t) \cap (s \cup u)$

Informal description

For any finite sets $s, t, u$ of a type $\alpha$, the following equality holds: $$ s \cup (t \cap u) = (s \cup t) \cap (s \cup u). $$

Finset.inter_union_distrib_right theorem

(s t u : Finset α) : s ∩ t ∪ u = (s ∪ u) ∩ (t ∪ u)

Full source

theorem inter_union_distrib_right (s t u : Finset α) : s ∩ ts ∩ t ∪ u = (s ∪ u) ∩ (t ∪ u) :=
  sup_inf_right _ _ _

Right Distributivity of Union over Intersection in Finite Sets: $(s \cap t) \cup u = (s \cup u) \cap (t \cup u)$

Informal description

For any finite sets $s, t, u$ of a type $\alpha$, the following equality holds: $$ (s \cap t) \cup u = (s \cup u) \cap (t \cup u). $$

Finset.union_union_distrib_left theorem

(s t u : Finset α) : s ∪ (t ∪ u) = s ∪ t ∪ (s ∪ u)

Full source

theorem union_union_distrib_left (s t u : Finset α) : s ∪ (t ∪ u) = s ∪ ts ∪ t ∪ (s ∪ u) :=
  sup_sup_distrib_left _ _ _

Left Distributivity of Union Operation on Finite Sets

Informal description

For any finite sets $s, t, u$ of type $\alpha$, the union operation satisfies the left distributivity property: $$ s \cup (t \cup u) = (s \cup t) \cup (s \cup u) $$

Finset.union_union_distrib_right theorem

(s t u : Finset α) : s ∪ t ∪ u = s ∪ u ∪ (t ∪ u)

Full source

theorem union_union_distrib_right (s t u : Finset α) : s ∪ ts ∪ t ∪ u = s ∪ us ∪ u ∪ (t ∪ u) :=
  sup_sup_distrib_right _ _ _

Right-Distributivity of Union Operation on Finite Sets

Informal description

For any finite sets $s, t, u$ of a type $\alpha$, the union operation satisfies the following right-distributivity property: $$s \cup t \cup u = s \cup u \cup (t \cup u)$$

Finset.inter_inter_distrib_left theorem

(s t u : Finset α) : s ∩ (t ∩ u) = s ∩ t ∩ (s ∩ u)

Full source

theorem inter_inter_distrib_left (s t u : Finset α) : s ∩ (t ∩ u) = s ∩ ts ∩ t ∩ (s ∩ u) :=
  inf_inf_distrib_left _ _ _

Left Distributivity of Intersection on Finite Sets: $s \cap (t \cap u) = (s \cap t) \cap (s \cap u)$

Informal description

For any finite sets $s, t, u$ of a type $\alpha$, the intersection operation satisfies the left distributivity property: $$ s \cap (t \cap u) = (s \cap t) \cap (s \cap u) $$

Finset.inter_inter_distrib_right theorem

(s t u : Finset α) : s ∩ t ∩ u = s ∩ u ∩ (t ∩ u)

Full source

theorem inter_inter_distrib_right (s t u : Finset α) : s ∩ ts ∩ t ∩ u = s ∩ us ∩ u ∩ (t ∩ u) :=
  inf_inf_distrib_right _ _ _

Right-Distributivity of Triple Intersection on Finite Sets

Informal description

For any finite sets $s, t, u$ of a type $\alpha$, the intersection operation satisfies the following right-distributivity property: $$ s \cap t \cap u = s \cap u \cap (t \cap u) $$

Finset.union_union_union_comm theorem

(s t u v : Finset α) : s ∪ t ∪ (u ∪ v) = s ∪ u ∪ (t ∪ v)

Full source

theorem union_union_union_comm (s t u v : Finset α) : s ∪ ts ∪ t ∪ (u ∪ v) = s ∪ us ∪ u ∪ (t ∪ v) :=
  sup_sup_sup_comm _ _ _ _

Commutativity of Quadruple Union Operation on Finite Sets

Informal description

For any finite sets $s, t, u, v$ of a type $\alpha$, the following equality holds: $$s \cup t \cup (u \cup v) = s \cup u \cup (t \cup v)$$

Finset.inter_inter_inter_comm theorem

(s t u v : Finset α) : s ∩ t ∩ (u ∩ v) = s ∩ u ∩ (t ∩ v)

Full source

theorem inter_inter_inter_comm (s t u v : Finset α) : s ∩ ts ∩ t ∩ (u ∩ v) = s ∩ us ∩ u ∩ (t ∩ v) :=
  inf_inf_inf_comm _ _ _ _

Commutativity of Quadruple Intersection Operation on Finite Sets

Informal description

For any finite sets $s, t, u, v$ of a type $\alpha$, the following equality holds: $$s \cap t \cap (u \cap v) = s \cap u \cap (t \cap v)$$

Finset.union_subset_iff theorem

: s ∪ t ⊆ u ↔ s ⊆ u ∧ t ⊆ u

Full source

theorem union_subset_iff : s ∪ ts ∪ t ⊆ us ∪ t ⊆ u ↔ s ⊆ u ∧ t ⊆ u :=
  (sup_le_iff : s ⊔ ts ⊔ t ≤ u ↔ s ≤ u ∧ t ≤ u)

Union Subset Criterion: $s \cup t \subseteq u \leftrightarrow (s \subseteq u \land t \subseteq u)$

Informal description

For any finite sets $s$, $t$, and $u$ of a type $\alpha$, the union $s \cup t$ is a subset of $u$ if and only if both $s \subseteq u$ and $t \subseteq u$.

Finset.subset_inter_iff theorem

: s ⊆ t ∩ u ↔ s ⊆ t ∧ s ⊆ u

Full source

theorem subset_inter_iff : s ⊆ t ∩ us ⊆ t ∩ u ↔ s ⊆ t ∧ s ⊆ u :=
  (le_inf_iff : s ≤ t ⊓ u ↔ s ≤ t ∧ s ≤ u)

Subset Criterion for Finite Set Intersection: $s \subseteq t \cap u \leftrightarrow (s \subseteq t \land s \subseteq u)$

Informal description

For any finite sets $s$, $t$, and $u$ of a type $\alpha$, the subset relation $s \subseteq t \cap u$ holds if and only if both $s \subseteq t$ and $s \subseteq u$ hold.

Finset.inter_eq_left theorem

: s ∩ t = s ↔ s ⊆ t

Full source

@[simp] lemma inter_eq_left : s ∩ ts ∩ t = s ↔ s ⊆ t := inf_eq_left

Intersection Equals Left Operand if and only if Left is Subset of Right

Informal description

For any finite sets $s$ and $t$ of a type $\alpha$, the intersection $s \cap t$ equals $s$ if and only if $s$ is a subset of $t$.

Finset.inter_eq_right theorem

: t ∩ s = s ↔ s ⊆ t

Full source

@[simp] lemma inter_eq_right : t ∩ st ∩ s = s ↔ s ⊆ t := inf_eq_right

Intersection Equals Right Operand if and only if Right is Subset of Left

Informal description

For any finite sets $s$ and $t$ of type $\alpha$, the intersection $t \cap s$ equals $s$ if and only if $s$ is a subset of $t$.

Finset.inter_congr_left theorem

(ht : s ∩ u ⊆ t) (hu : s ∩ t ⊆ u) : s ∩ t = s ∩ u

Full source

theorem inter_congr_left (ht : s ∩ us ∩ u ⊆ t) (hu : s ∩ ts ∩ t ⊆ u) : s ∩ t = s ∩ u :=
  inf_congr_left ht hu

Intersection Congruence under Left Absorption Conditions

Informal description

For any finite sets $s$, $t$, and $u$ of a type $\alpha$, if $s \cap u \subseteq t$ and $s \cap t \subseteq u$, then $s \cap t = s \cap u$.

Finset.inter_congr_right theorem

(hs : t ∩ u ⊆ s) (ht : s ∩ u ⊆ t) : s ∩ u = t ∩ u

Full source

theorem inter_congr_right (hs : t ∩ ut ∩ u ⊆ s) (ht : s ∩ us ∩ u ⊆ t) : s ∩ u = t ∩ u :=
  inf_congr_right hs ht

Intersection Congruence under Absorption Conditions

Informal description

For any finite sets $s$, $t$, and $u$ of type $\alpha$, if $t \cap u \subseteq s$ and $s \cap u \subseteq t$, then the intersections $s \cap u$ and $t \cap u$ are equal, i.e., $s \cap u = t \cap u$.

Finset.inter_eq_inter_iff_left theorem

: s ∩ t = s ∩ u ↔ s ∩ u ⊆ t ∧ s ∩ t ⊆ u

Full source

theorem inter_eq_inter_iff_left : s ∩ ts ∩ t = s ∩ u ↔ s ∩ u ⊆ t ∧ s ∩ t ⊆ u :=
  inf_eq_inf_iff_left

Intersection Equality under Left Absorption Conditions for Finite Sets

Informal description

For any finite sets $s$, $t$, and $u$ of a type $\alpha$, the equality $s \cap t = s \cap u$ holds if and only if $s \cap u \subseteq t$ and $s \cap t \subseteq u$.

Finset.inter_eq_inter_iff_right theorem

: s ∩ u = t ∩ u ↔ t ∩ u ⊆ s ∧ s ∩ u ⊆ t

Full source

theorem inter_eq_inter_iff_right : s ∩ us ∩ u = t ∩ u ↔ t ∩ u ⊆ s ∧ s ∩ u ⊆ t :=
  inf_eq_inf_iff_right

Intersection Equality Criterion via Absorption Conditions

Informal description

For any finite sets $s$, $t$, and $u$ of a type $\alpha$, the equality $s \cap u = t \cap u$ holds if and only if $t \cap u$ is a subset of $s$ and $s \cap u$ is a subset of $t$.

Finset.ite_subset_union theorem

(s s' : Finset α) (P : Prop) [Decidable P] : ite P s s' ⊆ s ∪ s'

Full source

theorem ite_subset_union (s s' : Finset α) (P : Prop) [Decidable P] : iteite P s s' ⊆ s ∪ s' :=
  ite_le_sup s s' P

Conditional Subset of Union in Finite Sets

Informal description

For any finite sets $s$ and $s'$ of type $\alpha$, and any decidable proposition $P$, the set $\text{ite}(P, s, s')$ (which equals $s$ if $P$ is true and $s'$ otherwise) is a subset of the union $s \cup s'$.

Finset.inter_subset_ite theorem

(s s' : Finset α) (P : Prop) [Decidable P] : s ∩ s' ⊆ ite P s s'

Full source

theorem inter_subset_ite (s s' : Finset α) (P : Prop) [Decidable P] : s ∩ s's ∩ s' ⊆ ite P s s' :=
  inf_le_ite s s' P

Intersection is Contained in Conditional Set for Finite Sets

Informal description

For any finite sets $s$ and $s'$ of type $\alpha$, and any decidable proposition $P$, the intersection $s \cap s'$ is a subset of the set $\text{ite}(P, s, s')$ (which equals $s$ if $P$ is true and $s'$ otherwise).

Mathlib.Data.Finset.Lattice.Basic

Main declarations

Operations on two or more finsets

Tags