Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
```/-
Authors: Yaël Dillies

! This file was ported from Lean 3 source module data.finset.pairwise
! leanprover-community/mathlib commit 9003f28797c0664a49e4179487267c494477d853
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Finset.Lattice

/-!
# Relations holding pairwise on finite sets

In this file we prove a few results about the interaction of `Set.PairwiseDisjoint` and `Finset`,
as well as the interaction of `List.Pairwise Disjoint` and the condition of
`Disjoint` on `List.toFinset`, in `Set` form.
-/

open Finset

variable {α: Type ?u.2α ι: Type ?u.3870ι ι': Type ?u.8ι' : Type _: Type (?u.3546+1)Type _}

instance: {α : Type u_1} →
[inst : DecidableEq α] →
{r : α → α → Prop} → [inst : DecidableRel r] → {s : Finset α} → Decidable (Set.Pairwise (↑s) r)instance [DecidableEq: Sort ?u.20 → Sort (max1?u.20)DecidableEq α: Type ?u.11α] {r: α → α → Propr : α: Type ?u.11α → α: Type ?u.11α → Prop: TypeProp} [DecidableRel: {α : Sort ?u.35} → (α → α → Prop) → Sort (max1?u.35)DecidableRel r: α → α → Propr] {s: Finset αs : Finset: Type ?u.51 → Type ?u.51Finset α: Type ?u.11α} :
Decidable: Prop → TypeDecidable ((s: Finset αs : Set: Type ?u.55 → Type ?u.55Set α: Type ?u.11α).Pairwise: {α : Type ?u.157} → Set α → (α → α → Prop) → PropPairwise r: α → α → Propr) :=
decidable_of_iff': {a : Prop} → (b : Prop) → (a ↔ b) → [inst : Decidable b] → Decidable adecidable_of_iff' (∀ a: ?m.180a ∈ s: Finset αs, ∀ b: ?m.213b ∈ s: Finset αs, a: ?m.180a ≠ b: ?m.213b → r: α → α → Propr a: ?m.180a b: ?m.213b) Iff.rfl: ∀ {a : Prop}, a ↔ aIff.rfl

theorem Finset.pairwiseDisjoint_range_singleton: ∀ {α : Type u_1}, Set.PairwiseDisjoint (Set.range singleton) idFinset.pairwiseDisjoint_range_singleton :
(Set.range: {α : Type ?u.1024} → {ι : Sort ?u.1023} → (ι → α) → Set αSet.range (singleton: {α : outParam (Type ?u.1032)} → {β : Type ?u.1031} → [self : Singleton α β] → α → βsingleton : α: Type ?u.1014α → Finset: Type ?u.1030 → Type ?u.1030Finset α: Type ?u.1014α)).PairwiseDisjoint: {α : Type ?u.1062} → {ι : Type ?u.1061} → [inst : PartialOrder α] → [inst : OrderBot α] → Set ι → (ι → α) → PropPairwiseDisjoint id: {α : Sort ?u.1145} → α → αid := byGoals accomplished! 🐙
α: Type u_1ι: Type ?u.1017ι': Type ?u.1020Set.PairwiseDisjoint (Set.range singleton) idrintro _: Finset α_ ⟨a, rfl⟩: x✝ ∈ Set.range singleton⟨a: αa⟨a, rfl⟩: x✝ ∈ Set.range singleton, rfl: {a} = x✝rfl⟨a, rfl⟩: x✝ ∈ Set.range singleton⟩ _: Finset α_ ⟨b, rfl⟩: y✝ ∈ Set.range singleton⟨b: αb⟨b, rfl⟩: y✝ ∈ Set.range singleton, rfl: {b} = y✝rfl⟨b, rfl⟩: y✝ ∈ Set.range singleton⟩ h: {a} ≠ {b}hα: Type u_1ι: Type ?u.1017ι': Type ?u.1020a, b: αh: {a} ≠ {b}intro.intro(Disjoint on id) {a} {b}
α: Type u_1ι: Type ?u.1017ι': Type ?u.1020Set.PairwiseDisjoint (Set.range singleton) idexact disjoint_singleton: ∀ {α : Type ?u.1270} {a b : α}, Disjoint {a} {b} ↔ a ≠ bdisjoint_singleton.2: ∀ {a b : Prop}, (a ↔ b) → b → a2 (ne_of_apply_ne: ∀ {α : Sort ?u.1296} {β : Sort ?u.1297} (f : α → β) {x y : α}, f x ≠ f y → x ≠ yne_of_apply_ne _: ?m.1298 → ?m.1299_ h: {a} ≠ {b}h)Goals accomplished! 🐙
#align finset.pairwise_disjoint_range_singleton Finset.pairwiseDisjoint_range_singleton: ∀ {α : Type u_1}, Set.PairwiseDisjoint (Set.range singleton) idFinset.pairwiseDisjoint_range_singleton

namespace Set

theorem PairwiseDisjoint.elim_finset: ∀ {s : Set ι} {f : ι → Finset α},
PairwiseDisjoint s f → ∀ {i j : ι}, i ∈ s → j ∈ s → ∀ (a : α), a ∈ f i → a ∈ f j → i = jPairwiseDisjoint.elim_finset {s: Set ιs : Set: Type ?u.1347 → Type ?u.1347Set ι: Type ?u.1341ι} {f: ι → Finset αf : ι: Type ?u.1341ι → Finset: Type ?u.1352 → Type ?u.1352Finset α: Type ?u.1338α} (hs: PairwiseDisjoint s fhs : s: Set ιs.PairwiseDisjoint: {α : Type ?u.1356} → {ι : Type ?u.1355} → [inst : PartialOrder α] → [inst : OrderBot α] → Set ι → (ι → α) → PropPairwiseDisjoint f: ι → Finset αf)
{i: ιi j: ιj : ι: Type ?u.1341ι} (hi: i ∈ shi : i: ιi ∈ s: Set ιs) (hj: j ∈ shj : j: ιj ∈ s: Set ιs) (a: αa : α: Type ?u.1338α) (hai: a ∈ f ihai : a: αa ∈ f: ι → Finset αf i: ιi) (haj: a ∈ f jhaj : a: αa ∈ f: ι → Finset αf j: ιj) : i: ιi = j: ιj :=
hs: PairwiseDisjoint s fhs.elim: ∀ {α : Type ?u.1596} {ι : Type ?u.1597} [inst : PartialOrder α] [inst_1 : OrderBot α] {s : Set ι} {f : ι → α},
PairwiseDisjoint s f → ∀ {i j : ι}, i ∈ s → j ∈ s → ¬Disjoint (f i) (f j) → i = jelim hi: i ∈ shi hj: j ∈ shj (Finset.not_disjoint_iff: ∀ {α : Type ?u.1668} {s t : Finset α}, ¬Disjoint s t ↔ ∃ a, a ∈ s ∧ a ∈ tFinset.not_disjoint_iff.2: ∀ {a b : Prop}, (a ↔ b) → b → a2 ⟨a: αa, hai: a ∈ f ihai, haj: a ∈ f jhaj⟩)
#align set.pairwise_disjoint.elim_finset Set.PairwiseDisjoint.elim_finset: ∀ {α : Type u_2} {ι : Type u_1} {s : Set ι} {f : ι → Finset α},
PairwiseDisjoint s f → ∀ {i j : ι}, i ∈ s → j ∈ s → ∀ (a : α), a ∈ f i → a ∈ f j → i = jSet.PairwiseDisjoint.elim_finset

theorem PairwiseDisjoint.image_finset_of_le: ∀ [inst : DecidableEq ι] [inst_1 : SemilatticeInf α] [inst_2 : OrderBot α] {s : Finset ι} {f : ι → α},
PairwiseDisjoint (↑s) f → ∀ {g : ι → ι}, (∀ (a : ι), f (g a) ≤ f a) → PairwiseDisjoint (↑(Finset.image g s)) fPairwiseDisjoint.image_finset_of_le [DecidableEq: Sort ?u.1731 → Sort (max1?u.1731)DecidableEq ι: Type ?u.1725ι] [SemilatticeInf: Type ?u.1740 → Type ?u.1740SemilatticeInf α: Type ?u.1722α] [OrderBot: (α : Type ?u.1743) → [inst : LE α] → Type ?u.1743OrderBot α: Type ?u.1722α]
{s: Finset ιs : Finset: Type ?u.2049 → Type ?u.2049Finset ι: Type ?u.1725ι} {f: ι → αf : ι: Type ?u.1725ι → α: Type ?u.1722α} (hs: PairwiseDisjoint (↑s) fhs : (s: Finset ιs : Set: Type ?u.2057 → Type ?u.2057Set ι: Type ?u.1725ι).PairwiseDisjoint: {α : Type ?u.2160} → {ι : Type ?u.2159} → [inst : PartialOrder α] → [inst : OrderBot α] → Set ι → (ι → α) → PropPairwiseDisjoint f: ι → αf) {g: ι → ιg : ι: Type ?u.1725ι → ι: Type ?u.1725ι}
(hf: ∀ (a : ι), f (g a) ≤ f ahf : ∀ a: ?m.2482a, f: ι → αf (g: ι → ιg a: ?m.2482a) ≤ f: ι → αf a: ?m.2482a) : (s: Finset ιs.image: {α : Type ?u.2723} → {β : Type ?u.2722} → [inst : DecidableEq β] → (α → β) → Finset α → Finset βimage g: ι → ιg : Set: Type ?u.2721 → Type ?u.2721Set ι: Type ?u.1725ι).PairwiseDisjoint: {α : Type ?u.2894} → {ι : Type ?u.2893} → [inst : PartialOrder α] → [inst : OrderBot α] → Set ι → (ι → α) → PropPairwiseDisjoint f: ι → αf := byGoals accomplished! 🐙
α: Type u_2ι: Type u_1ι': Type ?u.1728inst✝²: DecidableEq ιinst✝¹: SemilatticeInf αinst✝: OrderBot αs: Finset ιf: ι → αhs: PairwiseDisjoint (↑s) fg: ι → ιhf: ∀ (a : ι), f (g a) ≤ f aPairwiseDisjoint (↑(Finset.image g s)) frw [α: Type u_2ι: Type u_1ι': Type ?u.1728inst✝²: DecidableEq ιinst✝¹: SemilatticeInf αinst✝: OrderBot αs: Finset ιf: ι → αhs: PairwiseDisjoint (↑s) fg: ι → ιhf: ∀ (a : ι), f (g a) ≤ f aPairwiseDisjoint (↑(Finset.image g s)) fcoe_image: ∀ {α : Type ?u.3001} {β : Type ?u.3000} [inst : DecidableEq β] {s : Finset α} {f : α → β}, ↑(Finset.image f s) = f '' ↑scoe_imageα: Type u_2ι: Type u_1ι': Type ?u.1728inst✝²: DecidableEq ιinst✝¹: SemilatticeInf αinst✝: OrderBot αs: Finset ιf: ι → αhs: PairwiseDisjoint (↑s) fg: ι → ιhf: ∀ (a : ι), f (g a) ≤ f aPairwiseDisjoint (g '' ↑s) f]α: Type u_2ι: Type u_1ι': Type ?u.1728inst✝²: DecidableEq ιinst✝¹: SemilatticeInf αinst✝: OrderBot αs: Finset ιf: ι → αhs: PairwiseDisjoint (↑s) fg: ι → ιhf: ∀ (a : ι), f (g a) ≤ f aPairwiseDisjoint (g '' ↑s) f
α: Type u_2ι: Type u_1ι': Type ?u.1728inst✝²: DecidableEq ιinst✝¹: SemilatticeInf αinst✝: OrderBot αs: Finset ιf: ι → αhs: PairwiseDisjoint (↑s) fg: ι → ιhf: ∀ (a : ι), f (g a) ≤ f aPairwiseDisjoint (↑(Finset.image g s)) fexact hs: PairwiseDisjoint (↑s) fhs.image_of_le: ∀ {α : Type ?u.3162} {ι : Type ?u.3163} [inst : PartialOrder α] [inst_1 : OrderBot α] {s : Set ι} {f : ι → α},
PairwiseDisjoint s f → ∀ {g : ι → ι}, f ∘ g ≤ f → PairwiseDisjoint (g '' s) fimage_of_le hf: ∀ (a : ι), f (g a) ≤ f ahfGoals accomplished! 🐙
#align set.pairwise_disjoint.image_finset_of_le Set.PairwiseDisjoint.image_finset_of_le: ∀ {α : Type u_2} {ι : Type u_1} [inst : DecidableEq ι] [inst_1 : SemilatticeInf α] [inst_2 : OrderBot α] {s : Finset ι}
{f : ι → α},
PairwiseDisjoint (↑s) f → ∀ {g : ι → ι}, (∀ (a : ι), f (g a) ≤ f a) → PairwiseDisjoint (↑(Finset.image g s)) fSet.PairwiseDisjoint.image_finset_of_le

variable [Lattice: Type ?u.3549 → Type ?u.3549Lattice α: Type ?u.3867α] [OrderBot: (α : Type ?u.3879) → [inst : LE α] → Type ?u.3879OrderBot α: Type ?u.3540α]

/-- Bind operation for `Set.PairwiseDisjoint`. In a complete lattice, you can use
`Set.PairwiseDisjoint.biUnion`. -/
theorem PairwiseDisjoint.biUnion_finset: ∀ {α : Type u_3} {ι : Type u_2} {ι' : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] {s : Set ι'}
{g : ι' → Finset ι} {f : ι → α},
(PairwiseDisjoint s fun i' => sup (g i') f) →
(∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) f) → PairwiseDisjoint (iUnion fun i => iUnion fun h => ↑(g i)) fPairwiseDisjoint.biUnion_finset {s: Set ι's : Set: Type ?u.4194 → Type ?u.4194Set ι': Type ?u.3873ι'} {g: ι' → Finset ιg : ι': Type ?u.3873ι' → Finset: Type ?u.4199 → Type ?u.4199Finset ι: Type ?u.3870ι} {f: ι → αf : ι: Type ?u.3870ι → α: Type ?u.3867α}
(hs: PairwiseDisjoint s fun i' => sup (g i') fhs : s: Set ι's.PairwiseDisjoint: {α : Type ?u.4207} → {ι : Type ?u.4206} → [inst : PartialOrder α] → [inst : OrderBot α] → Set ι → (ι → α) → PropPairwiseDisjoint fun i': ι'i' : ι': Type ?u.3873ι' => (g: ι' → Finset ιg i': ι'i').sup: {α : Type ?u.4290} → {β : Type ?u.4289} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → αsup f: ι → αf)
(hg: ∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) fhg : ∀ i: ?m.4691i ∈ s: Set ι's, (g: ι' → Finset ιg i: ?m.4691i : Set: Type ?u.4726 → Type ?u.4726Set ι: Type ?u.3870ι).PairwiseDisjoint: {α : Type ?u.4829} → {ι : Type ?u.4828} → [inst : PartialOrder α] → [inst : OrderBot α] → Set ι → (ι → α) → PropPairwiseDisjoint f: ι → αf) : (⋃ i: ?m.4920i ∈ s: Set ι's, ↑(g: ι' → Finset ιg i: ?m.4920i)).PairwiseDisjoint: {α : Type ?u.5064} → {ι : Type ?u.5063} → [inst : PartialOrder α] → [inst : OrderBot α] → Set ι → (ι → α) → PropPairwiseDisjoint f: ι → αf := byGoals accomplished! 🐙
α: Type u_3ι: Type u_2ι': Type u_1inst✝¹: Lattice αinst✝: OrderBot αs: Set ι'g: ι' → Finset ιf: ι → αhs: PairwiseDisjoint s fun i' => sup (g i') fhg: ∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) fPairwiseDisjoint (iUnion fun i => iUnion fun h => ↑(g i)) frintro a: ιa ha: a ∈ iUnion fun i => iUnion fun h => ↑(g i)ha b: ιb hb: b ∈ iUnion fun i => iUnion fun h => ↑(g i)hb hab: a ≠ bhabα: Type u_3ι: Type u_2ι': Type u_1inst✝¹: Lattice αinst✝: OrderBot αs: Set ι'g: ι' → Finset ιf: ι → αhs: PairwiseDisjoint s fun i' => sup (g i') fhg: ∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) fa: ιha: a ∈ iUnion fun i => iUnion fun h => ↑(g i)b: ιhb: b ∈ iUnion fun i => iUnion fun h => ↑(g i)hab: a ≠ b(Disjoint on f) a b
α: Type u_3ι: Type u_2ι': Type u_1inst✝¹: Lattice αinst✝: OrderBot αs: Set ι'g: ι' → Finset ιf: ι → αhs: PairwiseDisjoint s fun i' => sup (g i') fhg: ∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) fPairwiseDisjoint (iUnion fun i => iUnion fun h => ↑(g i)) fsimp_rw [α: Type u_3ι: Type u_2ι': Type u_1inst✝¹: Lattice αinst✝: OrderBot αs: Set ι'g: ι' → Finset ιf: ι → αhs: PairwiseDisjoint s fun i' => sup (g i') fhg: ∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) fa: ιha: a ∈ iUnion fun i => iUnion fun h => ↑(g i)b: ιhb: b ∈ iUnion fun i => iUnion fun h => ↑(g i)hab: a ≠ b(Disjoint on f) a bSet.mem_iUnion: ∀ {α : Type ?u.5462} {ι : Sort ?u.5463} {x : α} {s : ι → Set α}, (x ∈ iUnion fun i => s i) ↔ ∃ i, x ∈ s iSet.mem_iUnionα: Type u_3ι: Type u_2ι': Type u_1inst✝¹: Lattice αinst✝: OrderBot αs: Set ι'g: ι' → Finset ιf: ι → αhs: PairwiseDisjoint s fun i' => sup (g i') fhg: ∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) fa, b: ιhab: a ≠ bha: ∃ i i_1, a ∈ ↑(g i)hb: ∃ i i_1, b ∈ ↑(g i)(Disjoint on f) a b] at ha: a ∈ iUnion fun i => iUnion fun h => ↑(g i)ha hb: b ∈ iUnion fun i => iUnion fun h => ↑(g i)hbα: Type u_3ι: Type u_2ι': Type u_1inst✝¹: Lattice αinst✝: OrderBot αs: Set ι'g: ι' → Finset ιf: ι → αhs: PairwiseDisjoint s fun i' => sup (g i') fhg: ∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) fa, b: ιhab: a ≠ bha: ∃ i i_1, a ∈ ↑(g i)hb: ∃ i i_1, b ∈ ↑(g i)(Disjoint on f) a b
α: Type u_3ι: Type u_2ι': Type u_1inst✝¹: Lattice αinst✝: OrderBot αs: Set ι'g: ι' → Finset ιf: ι → αhs: PairwiseDisjoint s fun i' => sup (g i') fhg: ∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) fPairwiseDisjoint (iUnion fun i => iUnion fun h => ↑(g i)) fobtain ⟨c, hc, ha⟩: ∃ i i_1, a ∈ ↑(g i)⟨c: ι'c⟨c, hc, ha⟩: ∃ i i_1, a ∈ ↑(g i), hc: c ∈ shc⟨c, hc, ha⟩: ∃ i i_1, a ∈ ↑(g i), ha: a ∈ ↑(g c)ha⟨c, hc, ha⟩: ∃ i i_1, a ∈ ↑(g i)⟩ := ha: ∃ i i_1, a ∈ ↑(g i)haα: Type u_3ι: Type u_2ι': Type u_1inst✝¹: Lattice αinst✝: OrderBot αs: Set ι'g: ι' → Finset ιf: ι → αhs: PairwiseDisjoint s fun i' => sup (g i') fhg: ∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) fa, b: ιhab: a ≠ bhb: ∃ i i_1, b ∈ ↑(g i)c: ι'hc: c ∈ sha: a ∈ ↑(g c)intro.intro(Disjoint on f) a b
α: Type u_3ι: Type u_2ι': Type u_1inst✝¹: Lattice αinst✝: OrderBot αs: Set ι'g: ι' → Finset ιf: ι → αhs: PairwiseDisjoint s fun i' => sup (g i') fhg: ∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) fPairwiseDisjoint (iUnion fun i => iUnion fun h => ↑(g i)) fobtain ⟨d, hd, hb⟩: ∃ i, b ∈ ↑(g d)⟨d: ι'd⟨d, hd, hb⟩: ∃ i, b ∈ ↑(g d), hd: d ∈ shd⟨d, hd, hb⟩: ∃ i, b ∈ ↑(g d), hb: b ∈ ↑(g d)hb⟨d, hd, hb⟩: ∃ i, b ∈ ↑(g d)⟩ := hb: ∃ i i_1, b ∈ ↑(g i)hbα: Type u_3ι: Type u_2ι': Type u_1inst✝¹: Lattice αinst✝: OrderBot αs: Set ι'g: ι' → Finset ιf: ι → αhs: PairwiseDisjoint s fun i' => sup (g i') fhg: ∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) fa, b: ιhab: a ≠ bc: ι'hc: c ∈ sha: a ∈ ↑(g c)d: ι'hd: d ∈ shb: b ∈ ↑(g d)intro.intro.intro.intro(Disjoint on f) a b
α: Type u_3ι: Type u_2ι': Type u_1inst✝¹: Lattice αinst✝: OrderBot αs: Set ι'g: ι' → Finset ιf: ι → αhs: PairwiseDisjoint s fun i' => sup (g i') fhg: ∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) fPairwiseDisjoint (iUnion fun i => iUnion fun h => ↑(g i)) fobtain hcd: g c = g dhcdhcd | hcd: g c = g d ∨ g c ≠ g d | hcd: g c ≠ g dhcd := eq_or_ne: ∀ {α : Sort ?u.6178} (x y : α), x = y ∨ x ≠ yeq_or_ne (g: ι' → Finset ιg c: ι'c) (g: ι' → Finset ιg d: ι'd)α: Type u_3ι: Type u_2ι': Type u_1inst✝¹: Lattice αinst✝: OrderBot αs: Set ι'g: ι' → Finset ιf: ι → αhs: PairwiseDisjoint s fun i' => sup (g i') fhg: ∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) fa, b: ιhab: a ≠ bc: ι'hc: c ∈ sha: a ∈ ↑(g c)d: ι'hd: d ∈ shb: b ∈ ↑(g d)hcd: g c = g dintro.intro.intro.intro.inl(Disjoint on f) a bα: Type u_3ι: Type u_2ι': Type u_1inst✝¹: Lattice αinst✝: OrderBot αs: Set ι'g: ι' → Finset ιf: ι → αhs: PairwiseDisjoint s fun i' => sup (g i') fhg: ∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) fa, b: ιhab: a ≠ bc: ι'hc: c ∈ sha: a ∈ ↑(g c)d: ι'hd: d ∈ shb: b ∈ ↑(g d)hcd: g c ≠ g dintro.intro.intro.intro.inr(Disjoint on f) a b
α: Type u_3ι: Type u_2ι': Type u_1inst✝¹: Lattice αinst✝: OrderBot αs: Set ι'g: ι' → Finset ιf: ι → αhs: PairwiseDisjoint s fun i' => sup (g i') fhg: ∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) fPairwiseDisjoint (iUnion fun i => iUnion fun h => ↑(g i)) f·α: Type u_3ι: Type u_2ι': Type u_1inst✝¹: Lattice αinst✝: OrderBot αs: Set ι'g: ι' → Finset ιf: ι → αhs: PairwiseDisjoint s fun i' => sup (g i') fhg: ∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) fa, b: ιhab: a ≠ bc: ι'hc: c ∈ sha: a ∈ ↑(g c)d: ι'hd: d ∈ shb: b ∈ ↑(g d)hcd: g c = g dintro.intro.intro.intro.inl(Disjoint on f) a b α: Type u_3ι: Type u_2ι': Type u_1inst✝¹: Lattice αinst✝: OrderBot αs: Set ι'g: ι' → Finset ιf: ι → αhs: PairwiseDisjoint s fun i' => sup (g i') fhg: ∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) fa, b: ιhab: a ≠ bc: ι'hc: c ∈ sha: a ∈ ↑(g c)d: ι'hd: d ∈ shb: b ∈ ↑(g d)hcd: g c = g dintro.intro.intro.intro.inl(Disjoint on f) a bα: Type u_3ι: Type u_2ι': Type u_1inst✝¹: Lattice αinst✝: OrderBot αs: Set ι'g: ι' → Finset ιf: ι → αhs: PairwiseDisjoint s fun i' => sup (g i') fhg: ∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) fa, b: ιhab: a ≠ bc: ι'hc: c ∈ sha: a ∈ ↑(g c)d: ι'hd: d ∈ shb: b ∈ ↑(g d)hcd: g c ≠ g dintro.intro.intro.intro.inr(Disjoint on f) a bexact hg: ∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) fhg d: ι'd hd: d ∈ shd (α: Type u_3ι: Type u_2ι': Type u_1inst✝¹: Lattice αinst✝: OrderBot αs: Set ι'g: ι' → Finset ιf: ι → αhs: PairwiseDisjoint s fun i' => sup (g i') fhg: ∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) fa, b: ιhab: a ≠ bc: ι'hc: c ∈ sha: a ∈ ↑(g c)d: ι'hd: d ∈ shb: b ∈ ↑(g d)hcd: g c = g dintro.intro.intro.intro.inl(Disjoint on f) a bbyGoals accomplished! 🐙 α: Type u_3ι: Type u_2ι': Type u_1inst✝¹: Lattice αinst✝: OrderBot αs: Set ι'g: ι' → Finset ιf: ι → αhs: PairwiseDisjoint s fun i' => sup (g i') fhg: ∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) fa, b: ιhab: a ≠ bc: ι'hc: c ∈ sha: a ∈ ↑(g c)d: ι'hd: d ∈ shb: b ∈ ↑(g d)hcd: g c = g da ∈ ↑(g d)rwa [α: Type u_3ι: Type u_2ι': Type u_1inst✝¹: Lattice αinst✝: OrderBot αs: Set ι'g: ι' → Finset ιf: ι → αhs: PairwiseDisjoint s fun i' => sup (g i') fhg: ∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) fa, b: ιhab: a ≠ bc: ι'hc: c ∈ sha: a ∈ ↑(g c)d: ι'hd: d ∈ shb: b ∈ ↑(g d)hcd: g c = g da ∈ ↑(g d)hcd: g c = g dhcdα: Type u_3ι: Type u_2ι': Type u_1inst✝¹: Lattice αinst✝: OrderBot αs: Set ι'g: ι' → Finset ιf: ι → αhs: PairwiseDisjoint s fun i' => sup (g i') fhg: ∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) fa, b: ιhab: a ≠ bc: ι'hc: c ∈ sd: ι'ha: a ∈ ↑(g d)hd: d ∈ shb: b ∈ ↑(g d)hcd: g c = g da ∈ ↑(g d)]α: Type u_3ι: Type u_2ι': Type u_1inst✝¹: Lattice αinst✝: OrderBot αs: Set ι'g: ι' → Finset ιf: ι → αhs: PairwiseDisjoint s fun i' => sup (g i') fhg: ∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) fa, b: ιhab: a ≠ bc: ι'hc: c ∈ sd: ι'ha: a ∈ ↑(g d)hd: d ∈ shb: b ∈ ↑(g d)hcd: g c = g da ∈ ↑(g d) at ha: a ∈ ↑(g c)haGoals accomplished! 🐙) hb: b ∈ ↑(g d)hb hab: a ≠ bhabGoals accomplished! 🐙
α: Type u_3ι: Type u_2ι': Type u_1inst✝¹: Lattice αinst✝: OrderBot αs: Set ι'g: ι' → Finset ιf: ι → αhs: PairwiseDisjoint s fun i' => sup (g i') fhg: ∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) fPairwiseDisjoint (iUnion fun i => iUnion fun h => ↑(g i)) f·α: Type u_3ι: Type u_2ι': Type u_1inst✝¹: Lattice αinst✝: OrderBot αs: Set ι'g: ι' → Finset ιf: ι → αhs: PairwiseDisjoint s fun i' => sup (g i') fhg: ∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) fa, b: ιhab: a ≠ bc: ι'hc: c ∈ sha: a ∈ ↑(g c)d: ι'hd: d ∈ shb: b ∈ ↑(g d)hcd: g c ≠ g dintro.intro.intro.intro.inr(Disjoint on f) a b α: Type u_3ι: Type u_2ι': Type u_1inst✝¹: Lattice αinst✝: OrderBot αs: Set ι'g: ι' → Finset ιf: ι → αhs: PairwiseDisjoint s fun i' => sup (g i') fhg: ∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) fa, b: ιhab: a ≠ bc: ι'hc: c ∈ sha: a ∈ ↑(g c)d: ι'hd: d ∈ shb: b ∈ ↑(g d)hcd: g c ≠ g dintro.intro.intro.intro.inr(Disjoint on f) a bexact (hs: PairwiseDisjoint s fun i' => sup (g i') fhs hc: c ∈ shc hd: d ∈ shd (ne_of_apply_ne: ∀ {α : Sort ?u.6306} {β : Sort ?u.6307} (f : α → β) {x y : α}, f x ≠ f y → x ≠ yne_of_apply_ne _: ?m.6308 → ?m.6309_ hcd: g c ≠ g dhcd)).mono: ∀ {α : Type ?u.6323} [inst : PartialOrder α] [inst_1 : OrderBot α] {a b c d : α},
a ≤ b → c ≤ d → Disjoint b d → Disjoint a cmono (Finset.le_sup: ∀ {α : Type ?u.6424} {β : Type ?u.6423} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {f : β → α}
{b : β}, b ∈ s → f b ≤ sup s fFinset.le_sup ha: a ∈ ↑(g c)ha) (Finset.le_sup: ∀ {α : Type ?u.6523} {β : Type ?u.6522} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {f : β → α}
{b : β}, b ∈ s → f b ≤ sup s fFinset.le_sup hb: b ∈ ↑(g d)hb)Goals accomplished! 🐙
#align set.pairwise_disjoint.bUnion_finset Set.PairwiseDisjoint.biUnion_finset: ∀ {α : Type u_3} {ι : Type u_2} {ι' : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] {s : Set ι'}
{g : ι' → Finset ι} {f : ι → α},
(PairwiseDisjoint s fun i' => sup (g i') f) →
(∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) f) → PairwiseDisjoint (iUnion fun i => iUnion fun h => ↑(g i)) fSet.PairwiseDisjoint.biUnion_finset

end Set

namespace List

variable {β: Type ?u.6961β : Type _: Type (?u.6961+1)Type _} [DecidableEq: Sort ?u.6964 → Sort (max1?u.6964)DecidableEq α: Type ?u.6982α] {r: α → α → Propr : α: Type ?u.6982α → α: Type ?u.6952α → Prop: TypeProp} {l: List αl : List: Type ?u.7438 → Type ?u.7438List α: Type ?u.6952α}

theorem pairwise_of_coe_toFinset_pairwise: ∀ {α : Type u_1} [inst : DecidableEq α] {r : α → α → Prop} {l : List α},
Set.Pairwise (↑(toFinset l)) r → Nodup l → Pairwise r lpairwise_of_coe_toFinset_pairwise (hl: Set.Pairwise (↑(toFinset l)) rhl : (l: List αl.toFinset: {α : Type ?u.7014} → [inst : DecidableEq α] → List α → Finset αtoFinset : Set: Type ?u.7013 → Type ?u.7013Set α: Type ?u.6982α).Pairwise: {α : Type ?u.7167} → Set α → (α → α → Prop) → PropPairwise r: α → α → Propr) (hn: Nodup lhn : l: List αl.Nodup: {α : Type ?u.7180} → List α → PropNodup) :
l: List αl.Pairwise: {α : Type ?u.7186} → (α → α → Prop) → List α → PropPairwise r: α → α → Propr := byGoals accomplished! 🐙
α: Type u_1ι: Type ?u.6985ι': Type ?u.6988β: Type ?u.6991inst✝: DecidableEq αr: α → α → Propl: List αhl: Set.Pairwise (↑(toFinset l)) rhn: Nodup lPairwise r lrw [α: Type u_1ι: Type ?u.6985ι': Type ?u.6988β: Type ?u.6991inst✝: DecidableEq αr: α → α → Propl: List αhl: Set.Pairwise (↑(toFinset l)) rhn: Nodup lPairwise r lcoe_toFinset: ∀ {α : Type ?u.7202} [inst : DecidableEq α] (l : List α), ↑(toFinset l) = { a | a ∈ l }coe_toFinsetα: Type u_1ι: Type ?u.6985ι': Type ?u.6988β: Type ?u.6991inst✝: DecidableEq αr: α → α → Propl: List αhl: Set.Pairwise { a | a ∈ l } rhn: Nodup lPairwise r l]α: Type u_1ι: Type ?u.6985ι': Type ?u.6988β: Type ?u.6991inst✝: DecidableEq αr: α → α → Propl: List αhl: Set.Pairwise { a | a ∈ l } rhn: Nodup lPairwise r l at hl: Set.Pairwise (↑(toFinset l)) rhlα: Type u_1ι: Type ?u.6985ι': Type ?u.6988β: Type ?u.6991inst✝: DecidableEq αr: α → α → Propl: List αhl: Set.Pairwise { a | a ∈ l } rhn: Nodup lPairwise r l
α: Type u_1ι: Type ?u.6985ι': Type ?u.6988β: Type ?u.6991inst✝: DecidableEq αr: α → α → Propl: List αhl: Set.Pairwise (↑(toFinset l)) rhn: Nodup lPairwise r lexact hn: Nodup lhn.pairwise_of_set_pairwise: ∀ {α : Type ?u.7372} {l : List α} {r : α → α → Prop}, Nodup l → Set.Pairwise { x | x ∈ l } r → Pairwise r lpairwise_of_set_pairwise hl: Set.Pairwise { a | a ∈ l } rhlGoals accomplished! 🐙
#align list.pairwise_of_coe_to_finset_pairwise List.pairwise_of_coe_toFinset_pairwise: ∀ {α : Type u_1} [inst : DecidableEq α] {r : α → α → Prop} {l : List α},
Set.Pairwise (↑(toFinset l)) r → Nodup l → Pairwise r lList.pairwise_of_coe_toFinset_pairwise

theorem pairwise_iff_coe_toFinset_pairwise: ∀ {α : Type u_1} [inst : DecidableEq α] {r : α → α → Prop} {l : List α},
Nodup l → Symmetric r → (Set.Pairwise (↑(toFinset l)) r ↔ Pairwise r l)pairwise_iff_coe_toFinset_pairwise (hn: Nodup lhn : l: List αl.Nodup: {α : Type ?u.7441} → List α → PropNodup) (hs: Symmetric rhs : Symmetric: {β : Sort ?u.7448} → (β → β → Prop) → PropSymmetric r: α → α → Propr) :
(l: List αl.toFinset: {α : Type ?u.7460} → [inst : DecidableEq α] → List α → Finset αtoFinset : Set: Type ?u.7459 → Type ?u.7459Set α: Type ?u.7411α).Pairwise: {α : Type ?u.7612} → Set α → (α → α → Prop) → PropPairwise r: α → α → Propr ↔ l: List αl.Pairwise: {α : Type ?u.7623} → (α → α → Prop) → List α → PropPairwise r: α → α → Propr := byGoals accomplished! 🐙
α: Type u_1ι: Type ?u.7414ι': Type ?u.7417β: Type ?u.7420inst✝: DecidableEq αr: α → α → Propl: List αhn: Nodup lhs: Symmetric rSet.Pairwise (↑(toFinset l)) r ↔ Pairwise r lletI : IsSymm: (α : Type ?u.7640) → (α → α → Prop) → PropIsSymm α: Type u_1α r: α → α → Propr := ⟨hs: Symmetric rhs⟩α: Type u_1ι: Type ?u.7414ι': Type ?u.7417β: Type ?u.7420inst✝: DecidableEq αr: α → α → Propl: List αhn: Nodup lhs: Symmetric rthis:= { symm := hs }: IsSymm α rSet.Pairwise (↑(toFinset l)) r ↔ Pairwise r l
α: Type u_1ι: Type ?u.7414ι': Type ?u.7417β: Type ?u.7420inst✝: DecidableEq αr: α → α → Propl: List αhn: Nodup lhs: Symmetric rSet.Pairwise (↑(toFinset l)) r ↔ Pairwise r lrw [α: Type u_1ι: Type ?u.7414ι': Type ?u.7417β: Type ?u.7420inst✝: DecidableEq αr: α → α → Propl: List αhn: Nodup lhs: Symmetric rthis:= { symm := hs }: IsSymm α rSet.Pairwise (↑(toFinset l)) r ↔ Pairwise r lcoe_toFinset: ∀ {α : Type ?u.7658} [inst : DecidableEq α] (l : List α), ↑(toFinset l) = { a | a ∈ l }coe_toFinset,α: Type u_1ι: Type ?u.7414ι': Type ?u.7417β: Type ?u.7420inst✝: DecidableEq αr: α → α → Propl: List αhn: Nodup lhs: Symmetric rthis:= { symm := hs }: IsSymm α rSet.Pairwise { a | a ∈ l } r ↔ Pairwise r l α: Type u_1ι: Type ?u.7414ι': Type ?u.7417β: Type ?u.7420inst✝: DecidableEq αr: α → α → Propl: List αhn: Nodup lhs: Symmetric rthis:= { symm := hs }: IsSymm α rSet.Pairwise (↑(toFinset l)) r ↔ Pairwise r lhn: Nodup lhn.pairwise_coe: ∀ {α : Type ?u.7810} {l : List α} {r : α → α → Prop} [inst : IsSymm α r],
Nodup l → (Set.Pairwise { a | a ∈ l } r ↔ Pairwise r l)pairwise_coeα: Type u_1ι: Type ?u.7414ι': Type ?u.7417β: Type ?u.7420inst✝: DecidableEq αr: α → α → Propl: List αhn: Nodup lhs: Symmetric rthis:= { symm := hs }: IsSymm α rPairwise r l ↔ Pairwise r l]Goals accomplished! 🐙
#align list.pairwise_iff_coe_to_finset_pairwise List.pairwise_iff_coe_toFinset_pairwise: ∀ {α : Type u_1} [inst : DecidableEq α] {r : α → α → Prop} {l : List α},
Nodup l → Symmetric r → (Set.Pairwise (↑(toFinset l)) r ↔ Pairwise r l)List.pairwise_iff_coe_toFinset_pairwise

theorem pairwise_disjoint_of_coe_toFinset_pairwiseDisjoint: ∀ {α : Type u_1} {ι : Type u_2} [inst : SemilatticeInf α] [inst_1 : OrderBot α] [inst_2 : DecidableEq ι] {l : List ι}
{f : ι → α}, Set.PairwiseDisjoint (↑(toFinset l)) f → Nodup l → Pairwise (_root_.Disjoint on f) lpairwise_disjoint_of_coe_toFinset_pairwiseDisjoint {α: ?m.7897α ι: Type u_2ι} [SemilatticeInf: Type ?u.7903 → Type ?u.7903SemilatticeInf α: ?m.7897α] [OrderBot: (α : Type ?u.7906) → [inst : LE α] → Type ?u.7906OrderBot α: ?m.7897α]
[DecidableEq: Sort ?u.8211 → Sort (max1?u.8211)DecidableEq ι: ?m.7900ι] {l: List ιl : List: Type ?u.8220 → Type ?u.8220List ι: ?m.7900ι} {f: ι → αf : ι: ?m.7900ι → α: ?m.7897α} (hl: Set.PairwiseDisjoint (↑(toFinset l)) fhl : (l: List ιl.toFinset: {α : Type ?u.8229} → [inst : DecidableEq α] → List α → Finset αtoFinset : Set: Type ?u.8228 → Type ?u.8228Set ι: ?m.7900ι).PairwiseDisjoint: {α : Type ?u.8384} → {ι : Type ?u.8383} → [inst : PartialOrder α] → [inst : OrderBot α] → Set ι → (ι → α) → PropPairwiseDisjoint f: ι → αf)
(hn: Nodup lhn : l: List ιl.Nodup: {α : Type ?u.8701} → List α → PropNodup) : l: List ιl.Pairwise: {α : Type ?u.8707} → (α → α → Prop) → List α → PropPairwise (_root_.Disjoint: {α : Type ?u.8722} → [inst : PartialOrder α] → [inst : OrderBot α] → α → α → Prop_root_.Disjoint on f: ι → αf) :=
pairwise_of_coe_toFinset_pairwise: ∀ {α : Type ?u.8886} [inst : DecidableEq α] {r : α → α → Prop} {l : List α},
Set.Pairwise (↑(toFinset l)) r → Nodup l → Pairwise r lpairwise_of_coe_toFinset_pairwise hl: Set.PairwiseDisjoint (↑(toFinset l)) fhl hn: Nodup lhn
#align list.pairwise_disjoint_of_coe_to_finset_pairwise_disjoint List.pairwise_disjoint_of_coe_toFinset_pairwiseDisjoint: ∀ {α : Type u_1} {ι : Type u_2} [inst : SemilatticeInf α] [inst_1 : OrderBot α] [inst_2 : DecidableEq ι] {l : List ι}
{f : ι → α}, Set.PairwiseDisjoint (↑(toFinset l)) f → Nodup l → Pairwise (_root_.Disjoint on f) lList.pairwise_disjoint_of_coe_toFinset_pairwiseDisjoint

theorem pairwiseDisjoint_iff_coe_toFinset_pairwise_disjoint: ∀ {α : Type u_1} {ι : Type u_2} [inst : SemilatticeInf α] [inst_1 : OrderBot α] [inst_2 : DecidableEq ι] {l : List ι}
{f : ι → α}, Nodup l → (Set.PairwiseDisjoint (↑(toFinset l)) f ↔ Pairwise (_root_.Disjoint on f) l)pairwiseDisjoint_iff_coe_toFinset_pairwise_disjoint {α: ?m.9049α ι: ?m.9052ι} [SemilatticeInf: Type ?u.9055 → Type ?u.9055SemilatticeInf α: ?m.9049α] [OrderBot: (α : Type ?u.9058) → [inst : LE α] → Type ?u.9058OrderBot α: ?m.9049α]
[DecidableEq: Sort ?u.9363 → Sort (max1?u.9363)DecidableEq ι: ?m.9052ι] {l: List ιl : List: Type ?u.9372 → Type ?u.9372List ι: ?m.9052ι} {f: ι → αf : ι: ?m.9052ι → α: ?m.9049α} (hn: Nodup lhn : l: List ιl.Nodup: {α : Type ?u.9379} → List α → PropNodup) :
(l: List ιl.toFinset: {α : Type ?u.9388} → [inst : DecidableEq α] → List α → Finset αtoFinset : Set: Type ?u.9387 → Type ?u.9387Set ι: ?m.9052ι).PairwiseDisjoint: {α : Type ?u.9542} → {ι : Type ?u.9541} → [inst : PartialOrder α] → [inst : OrderBot α] → Set ι → (ι → α) → PropPairwiseDisjoint f: ι → αf ↔ l: List ιl.Pairwise: {α : Type ?u.9789} → (α → α → Prop) → List α → PropPairwise (_root_.Disjoint: {α : Type ?u.9804} → [inst : PartialOrder α] → [inst : OrderBot α] → α → α → Prop_root_.Disjoint on f: ι → αf) :=
pairwise_iff_coe_toFinset_pairwise: ∀ {α : Type ?u.9967} [inst : DecidableEq α] {r : α → α → Prop} {l : List α},
Nodup l → Symmetric r → (Set.Pairwise (↑(toFinset l)) r ↔ Pairwise r l)pairwise_iff_coe_toFinset_pairwise hn: Nodup lhn (symmetric_disjoint: ∀ {α : Type ?u.10061} [inst : PartialOrder α] [inst_1 : OrderBot α], Symmetric _root_.Disjointsymmetric_disjoint.comap: ∀ {α : Type ?u.10134} {β : Type ?u.10133} {r : β → β → Prop}, Symmetric r → ∀ (f : α → β), Symmetric (r on f)comap f: ι → αf)
#align list.pairwise_disjoint_iff_coe_to_finset_pairwise_disjoint List.pairwiseDisjoint_iff_coe_toFinset_pairwise_disjoint: ∀ {α : Type u_1} {ι : Type u_2} [inst : SemilatticeInf α] [inst_1 : OrderBot α] [inst_2 : DecidableEq ι] {l : List ι}
{f : ι → α}, Nodup l → (Set.PairwiseDisjoint (↑(toFinset l)) f ↔ Pairwise (_root_.Disjoint on f) l)List.pairwiseDisjoint_iff_coe_toFinset_pairwise_disjoint

end List
```