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: Aaron Anderson, Kevin Buzzard, Yaël Dillies, Eric Wieser

! This file was ported from Lean 3 source module order.sup_indep
! leanprover-community/mathlib commit 1c857a1f6798cb054be942199463c2cf904cb937
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Finset.Pairwise
import Mathlib.Data.Finset.Powerset
import Mathlib.Data.Fintype.Basic

/-!
# Supremum independence

In this file, we define supremum independence of indexed sets. An indexed family `f : ι → α` is
sup-independent if, for all `a`, `f a` and the supremum of the rest are disjoint.

## Main definitions

* `Finset.SupIndep s f`: a family of elements `f` are supremum independent on the finite set `s`.
* `CompleteLattice.SetIndependent s`: a set of elements are supremum independent.
* `CompleteLattice.Independent f`: a family of elements are supremum independent.

## Main statements

* In a distributive lattice, supremum independence is equivalent to pairwise disjointness:
* `Finset.supIndep_iff_pairwiseDisjoint`
* `CompleteLattice.setIndependent_iff_pairwiseDisjoint`
* `CompleteLattice.independent_iff_pairwiseDisjoint`
* Otherwise, supremum independence is stronger than pairwise disjointness:
* `Finset.SupIndep.pairwiseDisjoint`
* `CompleteLattice.SetIndependent.pairwiseDisjoint`
* `CompleteLattice.Independent.pairwiseDisjoint`

## Implementation notes

For the finite version, we avoid the "obvious" definition
`∀ i ∈ s, Disjoint (f i) ((s.erase i).sup f)` because `erase` would require decidable equality on
`ι`.
-/

variable {α: Type ?u.24525α β: Type ?u.17β ι: Type ?u.8ι ι': Type ?u.24534ι' : Type _: Type (?u.51970+1)Type _}

/-! ### On lattices with a bottom element, via `Finset.sup` -/

namespace Finset

section Lattice

variable [Lattice: Type ?u.4788 → Type ?u.4788Lattice α: Type ?u.4776α] [OrderBot: (α : Type ?u.1607) → [inst : LE α] → Type ?u.1607OrderBot α: Type ?u.14α]

/-- Supremum independence of finite sets. We avoid the "obvious" definition using `s.erase i`
because `erase` would require decidable equality on `ι`. -/
def SupIndep: Finset ι → (ι → α) → PropSupIndep (s: Finset ιs : Finset: Type ?u.674 → Type ?u.674Finset ι: Type ?u.350ι) (f: ι → αf : ι: Type ?u.350ι → α: Type ?u.344α) : Prop: TypeProp :=
∀ ⦃t: ?m.685t⦄, t: ?m.685t ⊆ s: Finset ιs → ∀ ⦃i: ?m.707i⦄, i: ?m.707i ∈ s: Finset ιs → i: ?m.707i ∉ t: ?m.685t → Disjoint: {α : Type ?u.752} → [inst : PartialOrder α] → [inst : OrderBot α] → α → α → PropDisjoint (f: ι → αf i: ?m.707i) (t: ?m.685t.sup: {α : Type ?u.825} → {β : Type ?u.824} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → αsup f: ι → αf)
#align finset.sup_indep Finset.SupIndep: {α : Type u_1} → {ι : Type u_2} → [inst : Lattice α] → [inst : OrderBot α] → Finset ι → (ι → α) → PropFinset.SupIndep

variable {s: Finset ιs t: Finset ιt : Finset: Type ?u.5109 → Type ?u.5109Finset ι: Type ?u.1256ι} {f: ι → αf : ι: Type ?u.1598ι → α: Type ?u.4262α} {i: ιi : ι: Type ?u.4782ι}

instance: {α : Type u_1} →
{ι : Type u_2} →
[inst : Lattice α] →
[inst_1 : OrderBot α] →
{s : Finset ι} → {f : ι → α} → [inst_2 : DecidableEq ι] → [inst_3 : DecidableEq α] → Decidable (SupIndep s f)instance [DecidableEq: Sort ?u.1934 → Sort (max1?u.1934)DecidableEq ι: Type ?u.1598ι] [DecidableEq: Sort ?u.1943 → Sort (max1?u.1943)DecidableEq α: Type ?u.1592α] : Decidable: Prop → TypeDecidable (SupIndep: {α : Type ?u.1953} → {ι : Type ?u.1952} → [inst : Lattice α] → [inst : OrderBot α] → Finset ι → (ι → α) → PropSupIndep s: Finset ιs f: ι → αf) := byGoals accomplished! 🐙
α: Type ?u.1592β: Type ?u.1595ι: Type ?u.1598ι': Type ?u.1601inst✝³: Lattice αinst✝²: OrderBot αs, t: Finset ιf: ι → αi: ιinst✝¹: DecidableEq ιinst✝: DecidableEq αDecidable (SupIndep s f)refine @Finset.decidableForallOfDecidableSubsets: {α : Type ?u.1990} →
{s : Finset α} →
{p : (t : Finset α) → t ⊆ s → Prop} →
[inst : (t : Finset α) → (h : t ⊆ s) → Decidable (p t h)] → Decidable (∀ (t : Finset α) (h : t ⊆ s), p t h)Finset.decidableForallOfDecidableSubsets _: Type ?u.1990_ _: Finset ?m.1991_ _: (t : Finset ?m.1991) → t ⊆ ?m.1992 → Prop_ (?_: (t : Finset ?m.1991) → (h : t ⊆ ?m.1992) → Decidable (?m.1993 t h)?_)α: Type ?u.1592β: Type ?u.1595ι: Type ?u.1598ι': Type ?u.1601inst✝³: Lattice αinst✝²: OrderBot αs, t: Finset ιf: ι → αi: ιinst✝¹: DecidableEq ιinst✝: DecidableEq α(t : Finset ι) → t ⊆ s → Decidable (∀ ⦃i : ι⦄, i ∈ s → ¬i ∈ t → Disjoint (f i) (sup t f))
α: Type ?u.1592β: Type ?u.1595ι: Type ?u.1598ι': Type ?u.1601inst✝³: Lattice αinst✝²: OrderBot αs, t: Finset ιf: ι → αi: ιinst✝¹: DecidableEq ιinst✝: DecidableEq αDecidable (SupIndep s f)rintro t: Finset ?m.1991t -: t ⊆ ?m.1992-α: Type ?u.1592β: Type ?u.1595ι: Type ?u.1598ι': Type ?u.1601inst✝³: Lattice αinst✝²: OrderBot αs, t✝: Finset ιf: ι → αi: ιinst✝¹: DecidableEq ιinst✝: DecidableEq αt: Finset ιDecidable (∀ ⦃i : ι⦄, i ∈ s → ¬i ∈ t → Disjoint (f i) (sup t f))
α: Type ?u.1592β: Type ?u.1595ι: Type ?u.1598ι': Type ?u.1601inst✝³: Lattice αinst✝²: OrderBot αs, t: Finset ιf: ι → αi: ιinst✝¹: DecidableEq ιinst✝: DecidableEq αDecidable (SupIndep s f)refine @Finset.decidableDforallFinset: {α : Type ?u.2016} →
{s : Finset α} →
{p : (a : α) → a ∈ s → Prop} →
[_hp : (a : α) → (h : a ∈ s) → Decidable (p a h)] → Decidable (∀ (a : α) (h : a ∈ s), p a h)Finset.decidableDforallFinset _: Type ?u.2016_ _: Finset ?m.2017_ _: (a : ?m.2017) → a ∈ ?m.2018 → Prop_ (?_: (a : ?m.2017) → (h : a ∈ ?m.2018) → Decidable (?m.2019 a h)?_)α: Type ?u.1592β: Type ?u.1595ι: Type ?u.1598ι': Type ?u.1601inst✝³: Lattice αinst✝²: OrderBot αs, t✝: Finset ιf: ι → αi: ιinst✝¹: DecidableEq ιinst✝: DecidableEq αt: Finset ι(a : ι) → a ∈ s → Decidable (¬a ∈ t → Disjoint (f a) (sup t f))
α: Type ?u.1592β: Type ?u.1595ι: Type ?u.1598ι': Type ?u.1601inst✝³: Lattice αinst✝²: OrderBot αs, t: Finset ιf: ι → αi: ιinst✝¹: DecidableEq ιinst✝: DecidableEq αDecidable (SupIndep s f)rintro i: ?m.2017i -: i ∈ ?m.2018-α: Type ?u.1592β: Type ?u.1595ι: Type ?u.1598ι': Type ?u.1601inst✝³: Lattice αinst✝²: OrderBot αs, t✝: Finset ιf: ι → αi✝: ιinst✝¹: DecidableEq ιinst✝: DecidableEq αt: Finset ιi: ιDecidable (¬i ∈ t → Disjoint (f i) (sup t f))
α: Type ?u.1592β: Type ?u.1595ι: Type ?u.1598ι': Type ?u.1601inst✝³: Lattice αinst✝²: OrderBot αs, t: Finset ιf: ι → αi: ιinst✝¹: DecidableEq ιinst✝: DecidableEq αDecidable (SupIndep s f)have : Decidable: Prop → TypeDecidable (Disjoint: {α : Type ?u.2041} → [inst : PartialOrder α] → [inst : OrderBot α] → α → α → PropDisjoint (f: ι → αf i: ?m.2017i) (sup: {α : Type ?u.2046} → {β : Type ?u.2045} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → αsup t: Finset ?m.1991t f: ι → αf)) := decidable_of_iff': {a : Prop} → (b : Prop) → (a ↔ b) → [inst : Decidable b] → Decidable adecidable_of_iff' (_: ?m.2431_ = ⊥: ?m.2434⊥) disjoint_iff: ∀ {α : Type ?u.2507} [inst : SemilatticeInf α] [inst_1 : OrderBot α] {a b : α}, Disjoint a b ↔ a ⊓ b = ⊥disjoint_iffα: Type ?u.1592β: Type ?u.1595ι: Type ?u.1598ι': Type ?u.1601inst✝³: Lattice αinst✝²: OrderBot αs, t✝: Finset ιf: ι → αi✝: ιinst✝¹: DecidableEq ιinst✝: DecidableEq αt: Finset ιi: ιthis: Decidable (Disjoint (f i) (sup t f))Decidable (¬i ∈ t → Disjoint (f i) (sup t f))
α: Type ?u.1592β: Type ?u.1595ι: Type ?u.1598ι': Type ?u.1601inst✝³: Lattice αinst✝²: OrderBot αs, t: Finset ιf: ι → αi: ιinst✝¹: DecidableEq ιinst✝: DecidableEq αDecidable (SupIndep s f)infer_instanceGoals accomplished! 🐙

theorem SupIndep.subset: SupIndep t f → s ⊆ t → SupIndep s fSupIndep.subset (ht: SupIndep t fht : t: Finset ιt.SupIndep: {α : Type ?u.3984} → {ι : Type ?u.3983} → [inst : Lattice α] → [inst : OrderBot α] → Finset ι → (ι → α) → PropSupIndep f: ι → αf) (h: s ⊆ th : s: Finset ιs ⊆ t: Finset ιt) : s: Finset ιs.SupIndep: {α : Type ?u.4087} → {ι : Type ?u.4086} → [inst : Lattice α] → [inst : OrderBot α] → Finset ι → (ι → α) → PropSupIndep f: ι → αf := fun _: ?m.4156_ hu: ?m.4159hu _: ?m.4162_ hi: ?m.4165hi =>
ht: SupIndep t fht (hu: ?m.4159hu.trans: ∀ {α : Type ?u.4168} [inst : HasSubset α] [inst_1 : IsTrans α fun x x_1 => x ⊆ x_1] {a b c : α}, a ⊆ b → b ⊆ c → a ⊆ ctrans h: s ⊆ th) (h: s ⊆ th hi: ?m.4165hi)
#align finset.sup_indep.subset Finset.SupIndep.subset: ∀ {α : Type u_1} {ι : Type u_2} [inst : Lattice α] [inst_1 : OrderBot α] {s t : Finset ι} {f : ι → α},
SupIndep t f → s ⊆ t → SupIndep s fFinset.SupIndep.subset

theorem supIndep_empty: ∀ (f : ι → α), SupIndep ∅ fsupIndep_empty (f: ι → αf : ι: Type ?u.4268ι → α: Type ?u.4262α) : (∅: ?m.4611∅ : Finset: Type ?u.4609 → Type ?u.4609Finset ι: Type ?u.4268ι).SupIndep: {α : Type ?u.4657} → {ι : Type ?u.4656} → [inst : Lattice α] → [inst : OrderBot α] → Finset ι → (ι → α) → PropSupIndep f: ι → αf := fun _: ?m.4742_ _: ?m.4745_ a: ?m.4748a ha: ?m.4751ha =>
(not_mem_empty: ∀ {α : Type ?u.4753} (a : α), ¬a ∈ ∅not_mem_empty a: ?m.4748a ha: ?m.4751ha).elim: ∀ {C : Sort ?u.4755}, False → Celim
#align finset.sup_indep_empty Finset.supIndep_empty: ∀ {α : Type u_1} {ι : Type u_2} [inst : Lattice α] [inst_1 : OrderBot α] (f : ι → α), SupIndep ∅ fFinset.supIndep_empty

theorem supIndep_singleton: ∀ (i : ι) (f : ι → α), SupIndep {i} fsupIndep_singleton (i: ιi : ι: Type ?u.4782ι) (f: ι → αf : ι: Type ?u.4782ι → α: Type ?u.4776α) : ({i: ιi} : Finset: Type ?u.5125 → Type ?u.5125Finset ι: Type ?u.4782ι).SupIndep: {α : Type ?u.5152} → {ι : Type ?u.5151} → [inst : Lattice α] → [inst : OrderBot α] → Finset ι → (ι → α) → PropSupIndep f: ι → αf :=
fun s: ?m.5239s hs: ?m.5242hs j: ?m.5245j hji: ?m.5248hji hj: ?m.5251hj => byGoals accomplished! 🐙
α: Type u_1β: Type ?u.4779ι: Type u_2ι': Type ?u.4785inst✝¹: Lattice αinst✝: OrderBot αs✝, t: Finset ιf✝: ι → αi✝, i: ιf: ι → αs: Finset ιhs: s ⊆ {i}j: ιhji: j ∈ {i}hj: ¬j ∈ sDisjoint (f j) (sup s f)rw [α: Type u_1β: Type ?u.4779ι: Type u_2ι': Type ?u.4785inst✝¹: Lattice αinst✝: OrderBot αs✝, t: Finset ιf✝: ι → αi✝, i: ιf: ι → αs: Finset ιhs: s ⊆ {i}j: ιhji: j ∈ {i}hj: ¬j ∈ sDisjoint (f j) (sup s f)eq_empty_of_ssubset_singleton: ∀ {α : Type ?u.5261} {s : Finset α} {x : α}, s ⊂ {x} → s = ∅eq_empty_of_ssubset_singleton ⟨hs: s ⊆ {i}hs, fun h: ?m.5285h => hj: ¬j ∈ shj (h: ?m.5285h hji: j ∈ {i}hji)⟩,α: Type u_1β: Type ?u.4779ι: Type u_2ι': Type ?u.4785inst✝¹: Lattice αinst✝: OrderBot αs✝, t: Finset ιf✝: ι → αi✝, i: ιf: ι → αs: Finset ιhs: s ⊆ {i}j: ιhji: j ∈ {i}hj: ¬j ∈ sDisjoint (f j) (sup ∅ f) α: Type u_1β: Type ?u.4779ι: Type u_2ι': Type ?u.4785inst✝¹: Lattice αinst✝: OrderBot αs✝, t: Finset ιf✝: ι → αi✝, i: ιf: ι → αs: Finset ιhs: s ⊆ {i}j: ιhji: j ∈ {i}hj: ¬j ∈ sDisjoint (f j) (sup s f)sup_empty: ∀ {α : Type ?u.5299} {β : Type ?u.5300} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {f : β → α}, sup ∅ f = ⊥sup_emptyα: Type u_1β: Type ?u.4779ι: Type u_2ι': Type ?u.4785inst✝¹: Lattice αinst✝: OrderBot αs✝, t: Finset ιf✝: ι → αi✝, i: ιf: ι → αs: Finset ιhs: s ⊆ {i}j: ιhji: j ∈ {i}hj: ¬j ∈ sDisjoint (f j) ⊥]α: Type u_1β: Type ?u.4779ι: Type u_2ι': Type ?u.4785inst✝¹: Lattice αinst✝: OrderBot αs✝, t: Finset ιf✝: ι → αi✝, i: ιf: ι → αs: Finset ιhs: s ⊆ {i}j: ιhji: j ∈ {i}hj: ¬j ∈ sDisjoint (f j) ⊥
α: Type u_1β: Type ?u.4779ι: Type u_2ι': Type ?u.4785inst✝¹: Lattice αinst✝: OrderBot αs✝, t: Finset ιf✝: ι → αi✝, i: ιf: ι → αs: Finset ιhs: s ⊆ {i}j: ιhji: j ∈ {i}hj: ¬j ∈ sDisjoint (f j) (sup s f)exact disjoint_bot_right: ∀ {α : Type ?u.5445} [inst : PartialOrder α] [inst_1 : OrderBot α] {a : α}, Disjoint a ⊥disjoint_bot_rightGoals accomplished! 🐙
#align finset.sup_indep_singleton Finset.supIndep_singleton: ∀ {α : Type u_1} {ι : Type u_2} [inst : Lattice α] [inst_1 : OrderBot α] (i : ι) (f : ι → α), SupIndep {i} fFinset.supIndep_singleton

theorem SupIndep.pairwiseDisjoint: ∀ {α : Type u_1} {ι : Type u_2} [inst : Lattice α] [inst_1 : OrderBot α] {s : Finset ι} {f : ι → α},
SupIndep s f → Set.PairwiseDisjoint (↑s) fSupIndep.pairwiseDisjoint (hs: SupIndep s fhs : s: Finset ιs.SupIndep: {α : Type ?u.6186} → {ι : Type ?u.6185} → [inst : Lattice α] → [inst : OrderBot α] → Finset ι → (ι → α) → PropSupIndep f: ι → αf) : (s: Finset ιs : Set: Type ?u.6271 → Type ?u.6271Set ι: Type ?u.5849ι).PairwiseDisjoint: {α : Type ?u.6373} → {ι : Type ?u.6372} → [inst : PartialOrder α] → [inst : OrderBot α] → Set ι → (ι → α) → PropPairwiseDisjoint f: ι → αf :=
fun _: ?m.6758_ ha: ?m.6761ha _: ?m.6764_ hb: ?m.6767hb hab: ?m.6770hab =>
sup_singleton: ∀ {α : Type ?u.6772} {β : Type ?u.6773} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {f : β → α} {b : β},
sup {b} f = f bsup_singleton.subst: ∀ {α : Sort ?u.6830} {motive : α → Prop} {a b : α}, a = b → motive a → motive bsubst <| hs: SupIndep s fhs (singleton_subset_iff: ∀ {α : Type ?u.6847} {s : Finset α} {a : α}, {a} ⊆ s ↔ a ∈ ssingleton_subset_iff.2: ∀ {a b : Prop}, (a ↔ b) → b → a2 hb: ?m.6767hb) ha: ?m.6761ha <| not_mem_singleton: ∀ {α : Type ?u.6891} {a b : α}, ¬a ∈ {b} ↔ a ≠ bnot_mem_singleton.2: ∀ {a b : Prop}, (a ↔ b) → b → a2 hab: ?m.6770hab
#align finset.sup_indep.pairwise_disjoint Finset.SupIndep.pairwiseDisjoint: ∀ {α : Type u_1} {ι : Type u_2} [inst : Lattice α] [inst_1 : OrderBot α] {s : Finset ι} {f : ι → α},
SupIndep s f → Set.PairwiseDisjoint (↑s) fFinset.SupIndep.pairwiseDisjoint

/-- The RHS looks like the definition of `CompleteLattice.Independent`. -/
theorem supIndep_iff_disjoint_erase: ∀ {α : Type u_2} {ι : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] {s : Finset ι} {f : ι → α}
[inst_2 : DecidableEq ι], SupIndep s f ↔ ∀ (i : ι), i ∈ s → Disjoint (f i) (sup (erase s i) f)supIndep_iff_disjoint_erase [DecidableEq: Sort ?u.7295 → Sort (max1?u.7295)DecidableEq ι: Type ?u.6959ι] :
s: Finset ιs.SupIndep: {α : Type ?u.7305} → {ι : Type ?u.7304} → [inst : Lattice α] → [inst : OrderBot α] → Finset ι → (ι → α) → PropSupIndep f: ι → αf ↔ ∀ i: ?m.7339i ∈ s: Finset ιs, Disjoint: {α : Type ?u.7372} → [inst : PartialOrder α] → [inst : OrderBot α] → α → α → PropDisjoint (f: ι → αf i: ?m.7339i) ((s: Finset ιs.erase: {α : Type ?u.7444} → [inst : DecidableEq α] → Finset α → α → Finset αerase i: ?m.7339i).sup: {α : Type ?u.7492} → {β : Type ?u.7491} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → αsup f: ι → αf) :=
⟨fun hs: ?m.7891hs _: ?m.7894_ hi: ?m.7897hi => hs: ?m.7891hs (erase_subset: ∀ {α : Type ?u.7900} [inst : DecidableEq α] (a : α) (s : Finset α), erase s a ⊆ serase_subset _: ?m.7901_ _: Finset ?m.7901_) hi: ?m.7897hi (not_mem_erase: ∀ {α : Type ?u.8036} [inst : DecidableEq α] (a : α) (s : Finset α), ¬a ∈ erase s anot_mem_erase _: ?m.8037_ _: Finset ?m.8037_), fun hs: ?m.8134hs _: ?m.8139_ ht: ?m.8142ht i: ?m.8145i hi: ?m.8148hi hit: ?m.8151hit =>
(hs: ?m.8134hs i: ?m.8145i hi: ?m.8148hi).mono_right: ∀ {α : Type ?u.8153} [inst : PartialOrder α] [inst_1 : OrderBot α] {a b c : α}, b ≤ c → Disjoint a c → Disjoint a bmono_right (sup_mono: ∀ {α : Type ?u.8246} {β : Type ?u.8245} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s₁ s₂ : Finset β} {f : β → α},
s₁ ⊆ s₂ → sup s₁ f ≤ sup s₂ fsup_mono fun _: ?m.8317_ hj: ?m.8320hj => mem_erase: ∀ {α : Type ?u.8322} [inst : DecidableEq α] {a b : α} {s : Finset α}, a ∈ erase s b ↔ a ≠ b ∧ a ∈ smem_erase.2: ∀ {a b : Prop}, (a ↔ b) → b → a2 ⟨ne_of_mem_of_not_mem: ∀ {α : Type ?u.8417} {β : Type ?u.8418} [inst : Membership α β] {s : β} {a b : α}, a ∈ s → ¬b ∈ s → a ≠ bne_of_mem_of_not_mem hj: ?m.8320hj hit: ?m.8151hit, ht: ?m.8142ht hj: ?m.8320hj⟩)⟩
#align finset.sup_indep_iff_disjoint_erase Finset.supIndep_iff_disjoint_erase: ∀ {α : Type u_2} {ι : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] {s : Finset ι} {f : ι → α}
[inst_2 : DecidableEq ι], SupIndep s f ↔ ∀ (i : ι), i ∈ s → Disjoint (f i) (sup (erase s i) f)Finset.supIndep_iff_disjoint_erase

@[simp]
theorem supIndep_pair: ∀ {α : Type u_2} {ι : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] {f : ι → α} [inst_2 : DecidableEq ι] {i j : ι},
i ≠ j → (SupIndep {i, j} f ↔ Disjoint (f i) (f j))supIndep_pair [DecidableEq: Sort ?u.9172 → Sort (max1?u.9172)DecidableEq ι: Type ?u.8836ι] {i: ιi j: ιj : ι: Type ?u.8836ι} (hij: i ≠ jhij : i: ιi ≠ j: ιj) :
({i: ιi, j: ιj} : Finset: Type ?u.9190 → Type ?u.9190Finset ι: Type ?u.8836ι).SupIndep: {α : Type ?u.9269} → {ι : Type ?u.9268} → [inst : Lattice α] → [inst : OrderBot α] → Finset ι → (ι → α) → PropSupIndep f: ι → αf ↔ Disjoint: {α : Type ?u.9301} → [inst : PartialOrder α] → [inst : OrderBot α] → α → α → PropDisjoint (f: ι → αf i: ιi) (f: ι → αf j: ιj) :=
⟨fun h: ?m.9620h => h: ?m.9620h.pairwiseDisjoint: ∀ {α : Type ?u.9622} {ι : Type ?u.9623} [inst : Lattice α] [inst_1 : OrderBot α] {s : Finset ι} {f : ι → α},
SupIndep s f → Set.PairwiseDisjoint (↑s) fpairwiseDisjoint (byGoals accomplished! 🐙 α: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi✝: ιinst✝: DecidableEq ιi, j: ιhij: i ≠ jh: SupIndep {i, j} fi ∈ ↑{i, j}simpGoals accomplished! 🐙) (byGoals accomplished! 🐙 α: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi✝: ιinst✝: DecidableEq ιi, j: ιhij: i ≠ jh: SupIndep {i, j} fj ∈ ↑{i, j}simpGoals accomplished! 🐙) hij: i ≠ jhij,
fun h: ?m.9694h => byGoals accomplished! 🐙
α: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi✝: ιinst✝: DecidableEq ιi, j: ιhij: i ≠ jh: Disjoint (f i) (f j)SupIndep {i, j} frw [α: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi✝: ιinst✝: DecidableEq ιi, j: ιhij: i ≠ jh: Disjoint (f i) (f j)SupIndep {i, j} fsupIndep_iff_disjoint_erase: ∀ {α : Type ?u.10249} {ι : Type ?u.10248} [inst : Lattice α] [inst_1 : OrderBot α] {s : Finset ι} {f : ι → α}
[inst_2 : DecidableEq ι], SupIndep s f ↔ ∀ (i : ι), i ∈ s → Disjoint (f i) (sup (erase s i) f)supIndep_iff_disjoint_eraseα: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi✝: ιinst✝: DecidableEq ιi, j: ιhij: i ≠ jh: Disjoint (f i) (f j)∀ (i_1 : ι), i_1 ∈ {i, j} → Disjoint (f i_1) (sup (erase {i, j} i_1) f)]α: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi✝: ιinst✝: DecidableEq ιi, j: ιhij: i ≠ jh: Disjoint (f i) (f j)∀ (i_1 : ι), i_1 ∈ {i, j} → Disjoint (f i_1) (sup (erase {i, j} i_1) f)
α: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi✝: ιinst✝: DecidableEq ιi, j: ιhij: i ≠ jh: Disjoint (f i) (f j)SupIndep {i, j} fintro k: ιk hk: k ∈ {i, j}hkα: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi✝: ιinst✝: DecidableEq ιi, j: ιhij: i ≠ jh: Disjoint (f i) (f j)k: ιhk: k ∈ {i, j}Disjoint (f k) (sup (erase {i, j} k) f)
α: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi✝: ιinst✝: DecidableEq ιi, j: ιhij: i ≠ jh: Disjoint (f i) (f j)SupIndep {i, j} frw [α: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi✝: ιinst✝: DecidableEq ιi, j: ιhij: i ≠ jh: Disjoint (f i) (f j)k: ιhk: k ∈ {i, j}Disjoint (f k) (sup (erase {i, j} k) f)Finset.mem_insert: ∀ {α : Type ?u.10528} [inst : DecidableEq α] {s : Finset α} {a b : α}, a ∈ insert b s ↔ a = b ∨ a ∈ sFinset.mem_insert,α: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi✝: ιinst✝: DecidableEq ιi, j: ιhij: i ≠ jh: Disjoint (f i) (f j)k: ιhk: k = i ∨ k ∈ {j}Disjoint (f k) (sup (erase {i, j} k) f) α: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi✝: ιinst✝: DecidableEq ιi, j: ιhij: i ≠ jh: Disjoint (f i) (f j)k: ιhk: k ∈ {i, j}Disjoint (f k) (sup (erase {i, j} k) f)Finset.mem_singleton: ∀ {α : Type ?u.10702} {a b : α}, b ∈ {a} ↔ b = aFinset.mem_singletonα: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi✝: ιinst✝: DecidableEq ιi, j: ιhij: i ≠ jh: Disjoint (f i) (f j)k: ιhk: k = i ∨ k = jDisjoint (f k) (sup (erase {i, j} k) f)]α: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi✝: ιinst✝: DecidableEq ιi, j: ιhij: i ≠ jh: Disjoint (f i) (f j)k: ιhk: k = i ∨ k = jDisjoint (f k) (sup (erase {i, j} k) f) at hk: k = i ∨ k ∈ {j}hkα: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi✝: ιinst✝: DecidableEq ιi, j: ιhij: i ≠ jh: Disjoint (f i) (f j)k: ιhk: k = i ∨ k = jDisjoint (f k) (sup (erase {i, j} k) f)
α: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi✝: ιinst✝: DecidableEq ιi, j: ιhij: i ≠ jh: Disjoint (f i) (f j)SupIndep {i, j} fobtain rfl: k = irflrfl | rfl: k = i ∨ k = j | rfl: k = jrfl := hk: k = i ∨ k = jhkα: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi: ιinst✝: DecidableEq ιj, k: ιhij: k ≠ jh: Disjoint (f k) (f j)inlDisjoint (f k) (sup (erase {k, j} k) f)α: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi✝: ιinst✝: DecidableEq ιi, k: ιhij: i ≠ kh: Disjoint (f i) (f k)inrDisjoint (f k) (sup (erase {i, k} k) f)
α: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi✝: ιinst✝: DecidableEq ιi, j: ιhij: i ≠ jh: Disjoint (f i) (f j)SupIndep {i, j} f·α: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi: ιinst✝: DecidableEq ιj, k: ιhij: k ≠ jh: Disjoint (f k) (f j)inlDisjoint (f k) (sup (erase {k, j} k) f) α: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi: ιinst✝: DecidableEq ιj, k: ιhij: k ≠ jh: Disjoint (f k) (f j)inlDisjoint (f k) (sup (erase {k, j} k) f)α: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi✝: ιinst✝: DecidableEq ιi, k: ιhij: i ≠ kh: Disjoint (f i) (f k)inrDisjoint (f k) (sup (erase {i, k} k) f)convert h: Disjoint (f k) (f j)h using 1α: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi: ιinst✝: DecidableEq ιj, k: ιhij: k ≠ jh: Disjoint (f k) (f j)h.e'_5sup (erase {k, j} k) f = f j
α: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi: ιinst✝: DecidableEq ιj, k: ιhij: k ≠ jh: Disjoint (f k) (f j)inlDisjoint (f k) (sup (erase {k, j} k) f)rw [α: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi: ιinst✝: DecidableEq ιj, k: ιhij: k ≠ jh: Disjoint (f k) (f j)h.e'_5sup (erase {k, j} k) f = f jFinset.erase_insert: ∀ {α : Type ?u.11436} [inst : DecidableEq α] {a : α} {s : Finset α}, ¬a ∈ s → erase (insert a s) a = sFinset.erase_insert,α: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi: ιinst✝: DecidableEq ιj, k: ιhij: k ≠ jh: Disjoint (f k) (f j)h.e'_5sup {j} f = f jα: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi: ιinst✝: DecidableEq ιj, k: ιhij: k ≠ jh: Disjoint (f k) (f j)h.e'_5¬k ∈ {j} α: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi: ιinst✝: DecidableEq ιj, k: ιhij: k ≠ jh: Disjoint (f k) (f j)h.e'_5sup (erase {k, j} k) f = f jFinset.sup_singleton: ∀ {α : Type ?u.11612} {β : Type ?u.11613} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {f : β → α} {b : β},
sup {b} f = f bFinset.sup_singletonα: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi: ιinst✝: DecidableEq ιj, k: ιhij: k ≠ jh: Disjoint (f k) (f j)h.e'_5f j = f jα: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi: ιinst✝: DecidableEq ιj, k: ιhij: k ≠ jh: Disjoint (f k) (f j)h.e'_5¬k ∈ {j}]α: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi: ιinst✝: DecidableEq ιj, k: ιhij: k ≠ jh: Disjoint (f k) (f j)h.e'_5¬k ∈ {j}
α: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi: ιinst✝: DecidableEq ιj, k: ιhij: k ≠ jh: Disjoint (f k) (f j)inlDisjoint (f k) (sup (erase {k, j} k) f)simpa using hij: k ≠ jhijGoals accomplished! 🐙
α: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi✝: ιinst✝: DecidableEq ιi, j: ιhij: i ≠ jh: Disjoint (f i) (f j)SupIndep {i, j} f·α: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi✝: ιinst✝: DecidableEq ιi, k: ιhij: i ≠ kh: Disjoint (f i) (f k)inrDisjoint (f k) (sup (erase {i, k} k) f) α: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi✝: ιinst✝: DecidableEq ιi, k: ιhij: i ≠ kh: Disjoint (f i) (f k)inrDisjoint (f k) (sup (erase {i, k} k) f)convert h: Disjoint (f i) (f k)h.symm: ∀ {α : Type ?u.11850} [inst : PartialOrder α] [inst_1 : OrderBot α] ⦃a b : α⦄, Disjoint a b → Disjoint b asymm using 1α: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi✝: ιinst✝: DecidableEq ιi, k: ιhij: i ≠ kh: Disjoint (f i) (f k)h.e'_5sup (erase {i, k} k) f = f i
α: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi✝: ιinst✝: DecidableEq ιi, k: ιhij: i ≠ kh: Disjoint (f i) (f k)inrDisjoint (f k) (sup (erase {i, k} k) f)have : ({i: ιi, k: ιk} : Finset: Type ?u.12707 → Type ?u.12707Finset ι: Type u_1ι).erase: {α : Type ?u.12768} → [inst : DecidableEq α] → Finset α → α → Finset αerase k: ιk = {i: ιi} := α: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi✝: ιinst✝: DecidableEq ιi, k: ιhij: i ≠ kh: Disjoint (f i) (f k)h.e'_5sup (erase {i, k} k) f = f ibyGoals accomplished! 🐙
α: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi✝: ιinst✝: DecidableEq ιi, k: ιhij: i ≠ kh: Disjoint (f i) (f k)erase {i, k} k = {i}extα: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi✝: ιinst✝: DecidableEq ιi, k: ιhij: i ≠ kh: Disjoint (f i) (f k)a✝: ιaa✝ ∈ erase {i, k} k ↔ a✝ ∈ {i}
α: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi✝: ιinst✝: DecidableEq ιi, k: ιhij: i ≠ kh: Disjoint (f i) (f k)erase {i, k} k = {i}rw [α: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi✝: ιinst✝: DecidableEq ιi, k: ιhij: i ≠ kh: Disjoint (f i) (f k)a✝: ιaa✝ ∈ erase {i, k} k ↔ a✝ ∈ {i}mem_erase: ∀ {α : Type ?u.12873} [inst : DecidableEq α] {a b : α} {s : Finset α}, a ∈ erase s b ↔ a ≠ b ∧ a ∈ smem_erase,α: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi✝: ιinst✝: DecidableEq ιi, k: ιhij: i ≠ kh: Disjoint (f i) (f k)a✝: ιaa✝ ≠ k ∧ a✝ ∈ {i, k} ↔ a✝ ∈ {i} α: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi✝: ιinst✝: DecidableEq ιi, k: ιhij: i ≠ kh: Disjoint (f i) (f k)a✝: ιaa✝ ∈ erase {i, k} k ↔ a✝ ∈ {i}mem_insert: ∀ {α : Type ?u.13037} [inst : DecidableEq α] {s : Finset α} {a b : α}, a ∈ insert b s ↔ a = b ∨ a ∈ smem_insert,α: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi✝: ιinst✝: DecidableEq ιi, k: ιhij: i ≠ kh: Disjoint (f i) (f k)a✝: ιaa✝ ≠ k ∧ (a✝ = i ∨ a✝ ∈ {k}) ↔ a✝ ∈ {i} α: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi✝: ιinst✝: DecidableEq ιi, k: ιhij: i ≠ kh: Disjoint (f i) (f k)a✝: ιaa✝ ∈ erase {i, k} k ↔ a✝ ∈ {i}mem_singleton: ∀ {α : Type ?u.13201} {a b : α}, b ∈ {a} ↔ b = amem_singleton,α: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi✝: ιinst✝: DecidableEq ιi, k: ιhij: i ≠ kh: Disjoint (f i) (f k)a✝: ιaa✝ ≠ k ∧ (a✝ = i ∨ a✝ = k) ↔ a✝ ∈ {i} α: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi✝: ιinst✝: DecidableEq ιi, k: ιhij: i ≠ kh: Disjoint (f i) (f k)a✝: ιaa✝ ∈ erase {i, k} k ↔ a✝ ∈ {i}mem_singleton: ∀ {α : Type ?u.13208} {a b : α}, b ∈ {a} ↔ b = amem_singleton,α: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi✝: ιinst✝: DecidableEq ιi, k: ιhij: i ≠ kh: Disjoint (f i) (f k)a✝: ιaa✝ ≠ k ∧ (a✝ = i ∨ a✝ = k) ↔ a✝ = i α: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi✝: ιinst✝: DecidableEq ιi, k: ιhij: i ≠ kh: Disjoint (f i) (f k)a✝: ιaa✝ ∈ erase {i, k} k ↔ a✝ ∈ {i}and_or_left: ∀ {a b c : Prop}, a ∧ (b ∨ c) ↔ a ∧ b ∨ a ∧ cand_or_left,α: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi✝: ιinst✝: DecidableEq ιi, k: ιhij: i ≠ kh: Disjoint (f i) (f k)a✝: ιaa✝ ≠ k ∧ a✝ = i ∨ a✝ ≠ k ∧ a✝ = k ↔ a✝ = i α: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi✝: ιinst✝: DecidableEq ιi, k: ιhij: i ≠ kh: Disjoint (f i) (f k)a✝: ιaa✝ ∈ erase {i, k} k ↔ a✝ ∈ {i}Ne.def: ∀ {α : Sort ?u.13223} (a b : α), (a ≠ b) = ¬a = bNe.def,α: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi✝: ιinst✝: DecidableEq ιi, k: ιhij: i ≠ kh: Disjoint (f i) (f k)a✝: ιa¬a✝ = k ∧ a✝ = i ∨ ¬a✝ = k ∧ a✝ = k ↔ a✝ = i
α: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi✝: ιinst✝: DecidableEq ιi, k: ιhij: i ≠ kh: Disjoint (f i) (f k)a✝: ιaa✝ ∈ erase {i, k} k ↔ a✝ ∈ {i}not_and_self_iff: ∀ (a : Prop), ¬a ∧ a ↔ Falsenot_and_self_iff,α: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi✝: ιinst✝: DecidableEq ιi, k: ιhij: i ≠ kh: Disjoint (f i) (f k)a✝: ιa¬a✝ = k ∧ a✝ = i ∨ False ↔ a✝ = i α: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi✝: ιinst✝: DecidableEq ιi, k: ιhij: i ≠ kh: Disjoint (f i) (f k)a✝: ιaa✝ ∈ erase {i, k} k ↔ a✝ ∈ {i}or_false_iff: ∀ (p : Prop), p ∨ False ↔ por_false_iff,α: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi✝: ιinst✝: DecidableEq ιi, k: ιhij: i ≠ kh: Disjoint (f i) (f k)a✝: ιa¬a✝ = k ∧ a✝ = i ↔ a✝ = i α: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi✝: ιinst✝: DecidableEq ιi, k: ιhij: i ≠ kh: Disjoint (f i) (f k)a✝: ιaa✝ ∈ erase {i, k} k ↔ a✝ ∈ {i}and_iff_right_of_imp: ∀ {b a : Prop}, (b → a) → (a ∧ b ↔ b)and_iff_right_of_impα: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi✝: ιinst✝: DecidableEq ιi, k: ιhij: i ≠ kh: Disjoint (f i) (f k)a✝: ιaa✝ = i ↔ a✝ = iα: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi✝: ιinst✝: DecidableEq ιi, k: ιhij: i ≠ kh: Disjoint (f i) (f k)a✝: ιaa✝ = i → ¬a✝ = k]α: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi✝: ιinst✝: DecidableEq ιi, k: ιhij: i ≠ kh: Disjoint (f i) (f k)a✝: ιaa✝ = i → ¬a✝ = k
α: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi✝: ιinst✝: DecidableEq ιi, k: ιhij: i ≠ kh: Disjoint (f i) (f k)erase {i, k} k = {i}rintro rfl: ?m.13242rflα: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi: ιinst✝: DecidableEq ιk, a✝: ιhij: a✝ ≠ kh: Disjoint (f a✝) (f k)a¬a✝ = k
α: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi✝: ιinst✝: DecidableEq ιi, k: ιhij: i ≠ kh: Disjoint (f i) (f k)erase {i, k} k = {i}exact hij: a✝ ≠ khijGoals accomplished! 🐙
α: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi✝: ιinst✝: DecidableEq ιi, k: ιhij: i ≠ kh: Disjoint (f i) (f k)inrDisjoint (f k) (sup (erase {i, k} k) f)rw [α: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi✝: ιinst✝: DecidableEq ιi, k: ιhij: i ≠ kh: Disjoint (f i) (f k)this: erase {i, k} k = {i}h.e'_5sup (erase {i, k} k) f = f ithis: erase {i, k} k = ?m.12796this,α: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi✝: ιinst✝: DecidableEq ιi, k: ιhij: i ≠ kh: Disjoint (f i) (f k)this: erase {i, k} k = {i}h.e'_5sup {i} f = f i α: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi✝: ιinst✝: DecidableEq ιi, k: ιhij: i ≠ kh: Disjoint (f i) (f k)this: erase {i, k} k = {i}h.e'_5sup (erase {i, k} k) f = f iFinset.sup_singleton: ∀ {α : Type ?u.13280} {β : Type ?u.13281} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {f : β → α} {b : β},
sup {b} f = f bFinset.sup_singletonα: Type u_2β: Type ?u.8833ι: Type u_1ι': Type ?u.8839inst✝²: Lattice αinst✝¹: OrderBot αs, t: Finset ιf: ι → αi✝: ιinst✝: DecidableEq ιi, k: ιhij: i ≠ kh: Disjoint (f i) (f k)this: erase {i, k} k = {i}h.e'_5f i = f i]Goals accomplished! 🐙⟩
#align finset.sup_indep_pair Finset.supIndep_pair: ∀ {α : Type u_2} {ι : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] {f : ι → α} [inst_2 : DecidableEq ι] {i j : ι},
i ≠ j → (SupIndep {i, j} f ↔ Disjoint (f i) (f j))Finset.supIndep_pair

theorem supIndep_univ_bool: ∀ (f : Bool → α), SupIndep univ f ↔ Disjoint (f false) (f true)supIndep_univ_bool (f: Bool → αf : Bool: TypeBool → α: Type ?u.13540α) :
(Finset.univ: {α : Type ?u.13888} → [inst : Fintype α] → Finset αFinset.univ : Finset: Type ?u.13887 → Type ?u.13887Finset Bool: TypeBool).SupIndep: {α : Type ?u.13925} → {ι : Type ?u.13924} → [inst : Lattice α] → [inst : OrderBot α] → Finset ι → (ι → α) → PropSupIndep f: Bool → αf ↔ Disjoint: {α : Type ?u.13957} → [inst : PartialOrder α] → [inst : OrderBot α] → α → α → PropDisjoint (f: Bool → αf false: Boolfalse) (f: Bool → αf true: Booltrue) :=
haveI : true: Booltrue ≠ false: Boolfalse := byGoals accomplished! 🐙 α: Type u_1β: Type ?u.13543ι: Type ?u.13546ι': Type ?u.13549inst✝¹: Lattice αinst✝: OrderBot αs, t: Finset ιf✝: ι → αi: ιf: Bool → αtrue ≠ falsesimp only [Ne.def: ∀ {α : Sort ?u.14822} (a b : α), (a ≠ b) = ¬a = bNe.def, not_false_iff: ¬False ↔ Truenot_false_iff]Goals accomplished! 🐙
(supIndep_pair: ∀ {α : Type ?u.14268} {ι : Type ?u.14267} [inst : Lattice α] [inst_1 : OrderBot α] {f : ι → α} [inst_2 : DecidableEq ι]
{i j : ι}, i ≠ j → (SupIndep {i, j} f ↔ Disjoint (f i) (f j))supIndep_pair this: true ≠ falsethis).trans: ∀ {a b c : Prop}, (a ↔ b) → (b ↔ c) → (a ↔ c)trans disjoint_comm: ∀ {α : Type ?u.14417} [inst : PartialOrder α] [inst_1 : OrderBot α] {a b : α}, Disjoint a b ↔ Disjoint b adisjoint_comm
#align finset.sup_indep_univ_bool Finset.supIndep_univ_bool: ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] (f : Bool → α), SupIndep univ f ↔ Disjoint (f false) (f true)Finset.supIndep_univ_bool

@[simp]
theorem supIndep_univ_fin_two: ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] (f : Fin 2 → α), SupIndep univ f ↔ Disjoint (f 0) (f 1)supIndep_univ_fin_two (f: Fin 2 → αf : Fin: ℕ → TypeFin 2: ?m.152262 → α: Type ?u.14882α) :
(Finset.univ: {α : Type ?u.15243} → [inst : Fintype α] → Finset αFinset.univ : Finset: Type ?u.15239 → Type ?u.15239Finset (Fin: ℕ → TypeFin 2: ?m.152412)).SupIndep: {α : Type ?u.15283} → {ι : Type ?u.15282} → [inst : Lattice α] → [inst : OrderBot α] → Finset ι → (ι → α) → PropSupIndep f: Fin 2 → αf ↔ Disjoint: {α : Type ?u.15316} → [inst : PartialOrder α] → [inst : OrderBot α] → α → α → PropDisjoint (f: Fin 2 → αf 0: ?m.153210) (f: Fin 2 → αf 1: ?m.153471) :=
haveI : (0: ?m.156680 : Fin: ℕ → TypeFin 2: ?m.156652) ≠ 1: ?m.156711 := byGoals accomplished! 🐙 α: Type u_1β: Type ?u.14885ι: Type ?u.14888ι': Type ?u.14891inst✝¹: Lattice αinst✝: OrderBot αs, t: Finset ιf✝: ι → αi: ιf: Fin 2 → α0 ≠ 1simpGoals accomplished! 🐙
supIndep_pair: ∀ {α : Type ?u.15676} {ι : Type ?u.15675} [inst : Lattice α] [inst_1 : OrderBot α] {f : ι → α} [inst_2 : DecidableEq ι]
{i j : ι}, i ≠ j → (SupIndep {i, j} f ↔ Disjoint (f i) (f j))supIndep_pair this: 0 ≠ 1this
#align finset.sup_indep_univ_fin_two Finset.supIndep_univ_fin_two: ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] (f : Fin 2 → α), SupIndep univ f ↔ Disjoint (f 0) (f 1)Finset.supIndep_univ_fin_two

theorem SupIndep.attach: SupIndep s f → SupIndep (Finset.attach s) (f ∘ Subtype.val)SupIndep.attach (hs: SupIndep s fhs : s: Finset ιs.SupIndep: {α : Type ?u.16971} → {ι : Type ?u.16970} → [inst : Lattice α] → [inst : OrderBot α] → Finset ι → (ι → α) → PropSupIndep f: ι → αf) : s: Finset ιs.attach: {α : Type ?u.17055} → (s : Finset α) → Finset { x // x ∈ s }attach.SupIndep: {α : Type ?u.17058} → {ι : Type ?u.17057} → [inst : Lattice α] → [inst : OrderBot α] → Finset ι → (ι → α) → PropSupIndep (f: ι → αf ∘ Subtype.val: {α : Sort ?u.17129} → {p : α → Prop} → Subtype p → αSubtype.val) := byGoals accomplished! 🐙
α: Type u_1β: Type ?u.16631ι: Type u_2ι': Type ?u.16637inst✝¹: Lattice αinst✝: OrderBot αs, t: Finset ιf: ι → αi: ιhs: SupIndep s fSupIndep (Finset.attach s) (f ∘ Subtype.val)intro t: Finset { x // x ∈ s }t _: t ⊆ Finset.attach s_ i: { x // x ∈ s }i _: i ∈ Finset.attach s_ hi: ¬i ∈ thiα: Type u_1β: Type ?u.16631ι: Type u_2ι': Type ?u.16637inst✝¹: Lattice αinst✝: OrderBot αs, t✝: Finset ιf: ι → αi✝: ιhs: SupIndep s ft: Finset { x // x ∈ s }a✝¹: t ⊆ Finset.attach si: { x // x ∈ s }a✝: i ∈ Finset.attach shi: ¬i ∈ tDisjoint ((f ∘ Subtype.val) i) (sup t (f ∘ Subtype.val))
α: Type u_1β: Type ?u.16631ι: Type u_2ι': Type ?u.16637inst✝¹: Lattice αinst✝: OrderBot αs, t: Finset ιf: ι → αi: ιhs: SupIndep s fSupIndep (Finset.attach s) (f ∘ Subtype.val)classical
α: Type u_1β: Type ?u.16631ι: Type u_2ι': Type ?u.16637inst✝¹: Lattice αinst✝: OrderBot αs, t✝: Finset ιf: ι → αi✝: ιhs: SupIndep s ft: Finset { x // x ∈ s }a✝¹: t ⊆ Finset.attach si: { x // x ∈ s }a✝: i ∈ Finset.attach shi: ¬i ∈ tDisjoint ((f ∘ Subtype.val) i) (sup t (f ∘ Subtype.val))rw [α: Type u_1β: Type ?u.16631ι: Type u_2ι': Type ?u.16637inst✝¹: Lattice αinst✝: OrderBot αs, t✝: Finset ιf: ι → αi✝: ιhs: SupIndep s ft: Finset { x // x ∈ s }a✝¹: t ⊆ Finset.attach si: { x // x ∈ s }a✝: i ∈ Finset.attach shi: ¬i ∈ tDisjoint ((f ∘ Subtype.val) i) (sup t (f ∘ Subtype.val))← Finset.sup_image: ∀ {α : Type ?u.17170} {β : Type ?u.17168} {γ : Type ?u.17169} [inst : SemilatticeSup α] [inst_1 : OrderBot α]
[inst_2 : DecidableEq β] (s : Finset γ) (f : γ → β) (g : β → α), sup (image f s) g = sup s (g ∘ f)Finset.sup_imageα: Type u_1β: Type ?u.16631ι: Type u_2ι': Type ?u.16637inst✝¹: Lattice αinst✝: OrderBot αs, t✝: Finset ιf: ι → αi✝: ιhs: SupIndep s ft: Finset { x // x ∈ s }a✝¹: t ⊆ Finset.attach si: { x // x ∈ s }a✝: i ∈ Finset.attach shi: ¬i ∈ tDisjoint ((f ∘ Subtype.val) i) (sup (image Subtype.val t) f)]α: Type u_1β: Type ?u.16631ι: Type u_2ι': Type ?u.16637inst✝¹: Lattice αinst✝: OrderBot αs, t✝: Finset ιf: ι → αi✝: ιhs: SupIndep s ft: Finset { x // x ∈ s }a✝¹: t ⊆ Finset.attach si: { x // x ∈ s }a✝: i ∈ Finset.attach shi: ¬i ∈ tDisjoint ((f ∘ Subtype.val) i) (sup (image Subtype.val t) f)
α: Type u_1β: Type ?u.16631ι: Type u_2ι': Type ?u.16637inst✝¹: Lattice αinst✝: OrderBot αs, t✝: Finset ιf: ι → αi✝: ιhs: SupIndep s ft: Finset { x // x ∈ s }a✝¹: t ⊆ Finset.attach si: { x // x ∈ s }a✝: i ∈ Finset.attach shi: ¬i ∈ tDisjoint ((f ∘ Subtype.val) i) (sup t (f ∘ Subtype.val))refine' hs: SupIndep s fhs (image_subset_iff: ∀ {α : Type ?u.17646} {β : Type ?u.17645} [inst : DecidableEq β] {f : α → β} {s : Finset α} {t : Finset β},
image f s ⊆ t ↔ ∀ (x : α), x ∈ s → f x ∈ timage_subset_iff.2: ∀ {a b : Prop}, (a ↔ b) → b → a2 fun (j: { x // x ∈ s }j : { x: ?m.17746x // x: ?m.17746x ∈ s: Finset ιs }) _: ?m.17768_ => j: { x // x ∈ s }j.2: ∀ {α : Sort ?u.17770} {p : α → Prop} (self : Subtype p), p ↑self2) i: { x // x ∈ s }i.2: ∀ {α : Sort ?u.17819} {p : α → Prop} (self : Subtype p), p ↑self2 fun hi': ?m.17824hi' => hi: ¬i ∈ thi _: i ∈ t_α: Type u_1β: Type ?u.16631ι: Type u_2ι': Type ?u.16637inst✝¹: Lattice αinst✝: OrderBot αs, t✝: Finset ιf: ι → αi✝: ιhs: SupIndep s ft: Finset { x // x ∈ s }a✝¹: t ⊆ Finset.attach si: { x // x ∈ s }a✝: i ∈ Finset.attach shi: ¬i ∈ thi': ↑i ∈ image (fun j => ↑j) ti ∈ t
α: Type u_1β: Type ?u.16631ι: Type u_2ι': Type ?u.16637inst✝¹: Lattice αinst✝: OrderBot αs, t✝: Finset ιf: ι → αi✝: ιhs: SupIndep s ft: Finset { x // x ∈ s }a✝¹: t ⊆ Finset.attach si: { x // x ∈ s }a✝: i ∈ Finset.attach shi: ¬i ∈ tDisjoint ((f ∘ Subtype.val) i) (sup t (f ∘ Subtype.val))rw [α: Type u_1β: Type ?u.16631ι: Type u_2ι': Type ?u.16637inst✝¹: Lattice αinst✝: OrderBot αs, t✝: Finset ιf: ι → αi✝: ιhs: SupIndep s ft: Finset { x // x ∈ s }a✝¹: t ⊆ Finset.attach si: { x // x ∈ s }a✝: i ∈ Finset.attach shi: ¬i ∈ thi': ↑i ∈ image (fun j => ↑j) ti ∈ tmem_image: ∀ {α : Type ?u.17832} {β : Type ?u.17831} [inst : DecidableEq β] {f : α → β} {s : Finset α} {b : β},
b ∈ image f s ↔ ∃ a, a ∈ s ∧ f a = bmem_imageα: Type u_1β: Type ?u.16631ι: Type u_2ι': Type ?u.16637inst✝¹: Lattice αinst✝: OrderBot αs, t✝: Finset ιf: ι → αi✝: ιhs: SupIndep s ft: Finset { x // x ∈ s }a✝¹: t ⊆ Finset.attach si: { x // x ∈ s }a✝: i ∈ Finset.attach shi: ¬i ∈ thi': ∃ a, a ∈ t ∧ ↑a = ↑ii ∈ t]α: Type u_1β: Type ?u.16631ι: Type u_2ι': Type ?u.16637inst✝¹: Lattice αinst✝: OrderBot αs, t✝: Finset ιf: ι → αi✝: ιhs: SupIndep s ft: Finset { x // x ∈ s }a✝¹: t ⊆ Finset.attach si: { x // x ∈ s }a✝: i ∈ Finset.attach shi: ¬i ∈ thi': ∃ a, a ∈ t ∧ ↑a = ↑ii ∈ t at hi': ?m.17824hi'α: Type u_1β: Type ?u.16631ι: Type u_2ι': Type ?u.16637inst✝¹: Lattice αinst✝: OrderBot αs, t✝: Finset ιf: ι → αi✝: ιhs: SupIndep s ft: Finset { x // x ∈ s }a✝¹: t ⊆ Finset.attach si: { x // x ∈ s }a✝: i ∈ Finset.attach shi: ¬i ∈ thi': ∃ a, a ∈ t ∧ ↑a = ↑ii ∈ t
α: Type u_1β: Type ?u.16631ι: Type u_2ι': Type ?u.16637inst✝¹: Lattice αinst✝: OrderBot αs, t✝: Finset ιf: ι → αi✝: ιhs: SupIndep s ft: Finset { x // x ∈ s }a✝¹: t ⊆ Finset.attach si: { x // x ∈ s }a✝: i ∈ Finset.attach shi: ¬i ∈ tDisjoint ((f ∘ Subtype.val) i) (sup t (f ∘ Subtype.val))obtain ⟨j, hj, hji⟩: ∃ a, a ∈ t ∧ ↑a = ↑i⟨j: { x // x ∈ s }j⟨j, hj, hji⟩: ∃ a, a ∈ t ∧ ↑a = ↑i, hj: j ∈ thj⟨j, hj, hji⟩: ∃ a, a ∈ t ∧ ↑a = ↑i, hji: ↑j = ↑ihji⟨j, hj, hji⟩: ∃ a, a ∈ t ∧ ↑a = ↑i⟩ := hi': ∃ a, a ∈ t ∧ ↑a = ↑ihi'α: Type u_1β: Type ?u.16631ι: Type u_2ι': Type ?u.16637inst✝¹: Lattice αinst✝: OrderBot αs, t✝: Finset ιf: ι → αi✝: ιhs: SupIndep s ft: Finset { x // x ∈ s }a✝¹: t ⊆ Finset.attach si: { x // x ∈ s }a✝: i ∈ Finset.attach shi: ¬i ∈ tj: { x // x ∈ s }hj: j ∈ thji: ↑j = ↑iintro.introi ∈ t
α: Type u_1β: Type ?u.16631ι: Type u_2ι': Type ?u.16637inst✝¹: Lattice αinst✝: OrderBot αs, t✝: Finset ιf: ι → αi✝: ιhs: SupIndep s ft: Finset { x // x ∈ s }a✝¹: t ⊆ Finset.attach si: { x // x ∈ s }a✝: i ∈ Finset.attach shi: ¬i ∈ tDisjoint ((f ∘ Subtype.val) i) (sup t (f ∘ Subtype.val))rwa [α: Type u_1β: Type ?u.16631ι: Type u_2ι': Type ?u.16637inst✝¹: Lattice αinst✝: OrderBot αs, t✝: Finset ιf: ι → αi✝: ιhs: SupIndep s ft: Finset { x // x ∈ s }a✝¹: t ⊆ Finset.attach si: { x // x ∈ s }a✝: i ∈ Finset.attach shi: ¬i ∈ tj: { x // x ∈ s }hj: j ∈ thji: ↑j = ↑iintro.introi ∈ tSubtype.ext: ∀ {α : Sort ?u.18080} {p : α → Prop} {a1 a2 : { x // p x }}, ↑a1 = ↑a2 → a1 = a2Subtype.ext hji: ↑j = ↑ihjiα: Type u_1β: Type ?u.16631ι: Type u_2ι': Type ?u.16637inst✝¹: Lattice αinst✝: OrderBot αs, t✝: Finset ιf: ι → αi✝: ιhs: SupIndep s ft: Finset { x // x ∈ s }a✝¹: t ⊆ Finset.attach si: { x // x ∈ s }a✝: i ∈ Finset.attach shi: ¬i ∈ tj: { x // x ∈ s }hj: i ∈ thji: ↑j = ↑iintro.introi ∈ t]α: Type u_1β: Type ?u.16631ι: Type u_2ι': Type ?u.16637inst✝¹: Lattice αinst✝: OrderBot αs, t✝: Finset ιf: ι → αi✝: ιhs: SupIndep s ft: Finset { x // x ∈ s }a✝¹: t ⊆ Finset.attach si: { x // x ∈ s }a✝: i ∈ Finset.attach shi: ¬i ∈ tj: { x // x ∈ s }hj: i ∈ thji: ↑j = ↑iintro.introi ∈ t at hj: j ∈ thjGoals accomplished! 🐙
#align finset.sup_indep.attach Finset.SupIndep.attach: ∀ {α : Type u_1} {ι : Type u_2} [inst : Lattice α] [inst_1 : OrderBot α] {s : Finset ι} {f : ι → α},
SupIndep s f → SupIndep (attach s) (f ∘ Subtype.val)Finset.SupIndep.attach

end Lattice

section DistribLattice

variable [DistribLattice: Type ?u.18176 → Type ?u.18176DistribLattice α: Type ?u.22021α] [OrderBot: (α : Type ?u.18572) → [inst : LE α] → Type ?u.18572OrderBot α: Type ?u.18164α] {s: Finset ιs : Finset: Type ?u.20333 → Type ?u.20333Finset ι: Type ?u.18563ι} {f: ι → αf : ι: Type ?u.18170ι → α: Type ?u.18164α}

theorem supIndep_iff_pairwiseDisjoint: SupIndep s f ↔ Set.PairwiseDisjoint (↑s) fsupIndep_iff_pairwiseDisjoint : s: Finset ιs.SupIndep: {α : Type ?u.18951} → {ι : Type ?u.18950} → [inst : Lattice α] → [inst : OrderBot α] → Finset ι → (ι → α) → PropSupIndep f: ι → αf ↔ (s: Finset ιs : Set: Type ?u.19068 → Type ?u.19068Set ι: Type ?u.18563ι).PairwiseDisjoint: {α : Type ?u.19170} → {ι : Type ?u.19169} → [inst : PartialOrder α] → [inst : OrderBot α] → Set ι → (ι → α) → PropPairwiseDisjoint f: ι → αf :=
⟨SupIndep.pairwiseDisjoint: ∀ {α : Type ?u.19523} {ι : Type ?u.19524} [inst : Lattice α] [inst_1 : OrderBot α] {s : Finset ι} {f : ι → α},
SupIndep s f → Set.PairwiseDisjoint (↑s) fSupIndep.pairwiseDisjoint, fun hs: ?m.19712hs _: ?m.19715_ ht: ?m.19718ht _: ?m.19721_ hi: ?m.19724hi hit: ?m.19727hit =>
Finset.disjoint_sup_right: ∀ {α : Type ?u.19729} {ι : Type ?u.19730} [inst : DistribLattice α] [inst_1 : OrderBot α] {s : Finset ι} {f : ι → α}
{a : α}, Disjoint a (sup s f) ↔ ∀ ⦃i : ι⦄, i ∈ s → Disjoint a (f i)Finset.disjoint_sup_right.2: ∀ {a b : Prop}, (a ↔ b) → b → a2 fun _: ?m.19835_ hj: ?m.19838hj => hs: ?m.19712hs hi: ?m.19724hi (ht: ?m.19718ht hj: ?m.19838hj) (ne_of_mem_of_not_mem: ∀ {α : Type ?u.19856} {β : Type ?u.19857} [inst : Membership α β] {s : β} {a b : α}, a ∈ s → ¬b ∈ s → a ≠ bne_of_mem_of_not_mem hj: ?m.19838hj hit: ?m.19727hit).symm: ∀ {α : Sort ?u.19881} {a b : α}, a ≠ b → b ≠ asymm⟩
#align finset.sup_indep_iff_pairwise_disjoint Finset.supIndep_iff_pairwiseDisjoint: ∀ {α : Type u_1} {ι : Type u_2} [inst : DistribLattice α] [inst_1 : OrderBot α] {s : Finset ι} {f : ι → α},
SupIndep s f ↔ Set.PairwiseDisjoint (↑s) fFinset.supIndep_iff_pairwiseDisjoint

alias supIndep_iff_pairwiseDisjoint: ∀ {α : Type u_1} {ι : Type u_2} [inst : DistribLattice α] [inst_1 : OrderBot α] {s : Finset ι} {f : ι → α},
SupIndep s f ↔ Set.PairwiseDisjoint (↑s) fsupIndep_iff_pairwiseDisjoint ↔
sup_indep.pairwise_disjoint: ∀ {α : Type u_1} {ι : Type u_2} [inst : DistribLattice α] [inst_1 : OrderBot α] {s : Finset ι} {f : ι → α},
SupIndep s f → Set.PairwiseDisjoint (↑s) fsup_indep.pairwise_disjoint _root_.Set.PairwiseDisjoint.supIndep: ∀ {α : Type u_1} {ι : Type u_2} [inst : DistribLattice α] [inst_1 : OrderBot α] {s : Finset ι} {f : ι → α},
Set.PairwiseDisjoint (↑s) f → SupIndep s f_root_.Set.PairwiseDisjoint.supIndep
#align set.pairwise_disjoint.sup_indep Set.PairwiseDisjoint.supIndep: ∀ {α : Type u_1} {ι : Type u_2} [inst : DistribLattice α] [inst_1 : OrderBot α] {s : Finset ι} {f : ι → α},
Set.PairwiseDisjoint (↑s) f → SupIndep s fSet.PairwiseDisjoint.supIndep

/-- Bind operation for `SupIndep`. -/
theorem SupIndep.sup: ∀ {α : Type u_3} {ι : Type u_1} {ι' : Type u_2} [inst : DistribLattice α] [inst_1 : OrderBot α] [inst_2 : DecidableEq ι]
{s : Finset ι'} {g : ι' → Finset ι} {f : ι → α},
(SupIndep s fun i => Finset.sup (g i) f) → (∀ (i' : ι'), i' ∈ s → SupIndep (g i') f) → SupIndep (Finset.sup s g) fSupIndep.sup [DecidableEq: Sort ?u.20340 → Sort (max1?u.20340)DecidableEq ι: Type ?u.19953ι] {s: Finset ι's : Finset: Type ?u.20349 → Type ?u.20349Finset ι': Type ?u.19956ι'} {g: ι' → Finset ιg : ι': Type ?u.19956ι' → Finset: Type ?u.20354 → Type ?u.20354Finset ι: Type ?u.19953ι} {f: ι → αf : ι: Type ?u.19953ι → α: Type ?u.19947α}
(hs: SupIndep s fun i => Finset.sup (g i) fhs : s: Finset ι's.SupIndep: {α : Type ?u.20362} → {ι : Type ?u.20361} → [inst : Lattice α] → [inst : OrderBot α] → Finset ι → (ι → α) → PropSupIndep fun i: ?m.20426i => (g: ι' → Finset ιg i: ?m.20426i).sup: {α : Type ?u.20429} → {β : Type ?u.20428} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → αsup f: ι → αf) (hg: ∀ (i' : ι'), i' ∈ s → SupIndep (g i') fhg : ∀ i': ?m.20678i' ∈ s: Finset ι's, (g: ι' → Finset ιg i': ?m.20678i').SupIndep: {α : Type ?u.20712} → {ι : Type ?u.20711} → [inst : Lattice α] → [inst : OrderBot α] → Finset ι → (ι → α) → PropSupIndep f: ι → αf) :
(s: Finset ι's.sup: {α : Type ?u.20782} → {β : Type ?u.20781} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → αsup g: ι' → Finset ιg).SupIndep: {α : Type ?u.20860} → {ι : Type ?u.20859} → [inst : Lattice α] → [inst : OrderBot α] → Finset ι → (ι → α) → PropSupIndep f: ι → αf := byGoals accomplished! 🐙
α: Type u_3β: Type ?u.19950ι: Type u_1ι': Type u_2inst✝²: DistribLattice αinst✝¹: OrderBot αs✝: Finset ιf✝: ι → αinst✝: DecidableEq ιs: Finset ι'g: ι' → Finset ιf: ι → αhs: SupIndep s fun i => Finset.sup (g i) fhg: ∀ (i' : ι'), i' ∈ s → SupIndep (g i') fSupIndep (Finset.sup s g) fsimp_rw [α: Type u_3β: Type ?u.19950ι: Type u_1ι': Type u_2inst✝²: DistribLattice αinst✝¹: OrderBot αs✝: Finset ιf✝: ι → αinst✝: DecidableEq ιs: Finset ι'g: ι' → Finset ιf: ι → αhs: SupIndep s fun i => Finset.sup (g i) fhg: ∀ (i' : ι'), i' ∈ s → SupIndep (g i') fSupIndep (Finset.sup s g) fsupIndep_iff_pairwiseDisjoint: ∀ {α : Type ?u.21075} {ι : Type ?u.21076} [inst : DistribLattice α] [inst_1 : OrderBot α] {s : Finset ι} {f : ι → α},
SupIndep s f ↔ Set.PairwiseDisjoint (↑s) fsupIndep_iff_pairwiseDisjointα: Type u_3β: Type ?u.19950ι: Type u_1ι': Type u_2inst✝²: DistribLattice αinst✝¹: OrderBot αs✝: Finset ιf✝: ι → αinst✝: DecidableEq ιs: Finset ι'g: ι' → Finset ιf: ι → αhs: Set.PairwiseDisjoint ↑s fun i => Finset.sup (g i) fhg: ∀ (i' : ι'), i' ∈ s → Set.PairwiseDisjoint (↑(g i')) fSet.PairwiseDisjoint (↑(Finset.sup s g)) f] at hs: SupIndep s fun i => Finset.sup (g i) fhs hg: ∀ (i' : ι'), i' ∈ s → SupIndep (g i') fhg⊢α: Type u_3β: Type ?u.19950ι: Type u_1ι': Type u_2inst✝²: DistribLattice αinst✝¹: OrderBot αs✝: Finset ιf✝: ι → αinst✝: DecidableEq ιs: Finset ι'g: ι' → Finset ιf: ι → αhs: Set.PairwiseDisjoint ↑s fun i => Finset.sup (g i) fhg: ∀ (i' : ι'), i' ∈ s → Set.PairwiseDisjoint (↑(g i')) fSet.PairwiseDisjoint (↑(Finset.sup s g)) f
α: Type u_3β: Type ?u.19950ι: Type u_1ι': Type u_2inst✝²: DistribLattice αinst✝¹: OrderBot αs✝: Finset ιf✝: ι → αinst✝: DecidableEq ιs: Finset ι'g: ι' → Finset ιf: ι → αhs: SupIndep s fun i => Finset.sup (g i) fhg: ∀ (i' : ι'), i' ∈ s → SupIndep (g i') fSupIndep (Finset.sup s g) frw [α: Type u_3β: Type ?u.19950ι: Type u_1ι': Type u_2inst✝²: DistribLattice αinst✝¹: OrderBot αs✝: Finset ιf✝: ι → αinst✝: DecidableEq ιs: Finset ι'g: ι' → Finset ιf: ι → αhs: Set.PairwiseDisjoint ↑s fun i => Finset.sup (g i) fhg: ∀ (i' : ι'), i' ∈ s → Set.PairwiseDisjoint (↑(g i')) fSet.PairwiseDisjoint (↑(Finset.sup s g)) fsup_eq_biUnion: ∀ {α : Type ?u.21418} {β : Type ?u.21419} [inst : DecidableEq β] (s : Finset α) (t : α → Finset β),
Finset.sup s t = Finset.biUnion s tsup_eq_biUnion,α: Type u_3β: Type ?u.19950ι: Type u_1ι': Type u_2inst✝²: DistribLattice αinst✝¹: OrderBot αs✝: Finset ιf✝: ι → αinst✝: DecidableEq ιs: Finset ι'g: ι' → Finset ιf: ι → αhs: Set.PairwiseDisjoint ↑s fun i => Finset.sup (g i) fhg: ∀ (i' : ι'), i' ∈ s → Set.PairwiseDisjoint (↑(g i')) fSet.PairwiseDisjoint (↑(Finset.biUnion s g)) f α: Type u_3β: Type ?u.19950ι: Type u_1ι': Type u_2inst✝²: DistribLattice αinst✝¹: OrderBot αs✝: Finset ιf✝: ι → αinst✝: DecidableEq ιs: Finset ι'g: ι' → Finset ιf: ι → αhs: Set.PairwiseDisjoint ↑s fun i => Finset.sup (g i) fhg: ∀ (i' : ι'), i' ∈ s → Set.PairwiseDisjoint (↑(g i')) fSet.PairwiseDisjoint (↑(Finset.sup s g)) fcoe_biUnion: ∀ {α : Type ?u.21629} {β : Type ?u.21628} [inst : DecidableEq β] {s : Finset α} {t : α → Finset β},
↑(Finset.biUnion s t) = Set.iUnion fun x => Set.iUnion fun h => ↑(t x)coe_biUnionα: Type u_3β: Type ?u.19950ι: Type u_1ι': Type u_2inst✝²: DistribLattice αinst✝¹: OrderBot αs✝: Finset ιf✝: ι → αinst✝: DecidableEq ιs: Finset ι'g: ι' → Finset ιf: ι → αhs: Set.PairwiseDisjoint ↑s fun i => Finset.sup (g i) fhg: ∀ (i' : ι'), i' ∈ s → Set.PairwiseDisjoint (↑(g i')) fSet.PairwiseDisjoint (Set.iUnion fun x => Set.iUnion fun h => ↑(g x)) f]α: Type u_3β: Type ?u.19950ι: Type u_1ι': Type u_2inst✝²: DistribLattice αinst✝¹: OrderBot αs✝: Finset ιf✝: ι → αinst✝: DecidableEq ιs: Finset ι'g: ι' → Finset ιf: ι → αhs: Set.PairwiseDisjoint ↑s fun i => Finset.sup (g i) fhg: ∀ (i' : ι'), i' ∈ s → Set.PairwiseDisjoint (↑(g i')) fSet.PairwiseDisjoint (Set.iUnion fun x => Set.iUnion fun h => ↑(g x)) f
α: Type u_3β: Type ?u.19950ι: Type u_1ι': Type u_2inst✝²: DistribLattice αinst✝¹: OrderBot αs✝: Finset ιf✝: ι → αinst✝: DecidableEq ιs: Finset ι'g: ι' → Finset ιf: ι → αhs: SupIndep s fun i => Finset.sup (g i) fhg: ∀ (i' : ι'), i' ∈ s → SupIndep (g i') fSupIndep (Finset.sup s g) fexact hs: Set.PairwiseDisjoint ↑s fun i => Finset.sup (g i) fhs.biUnion_finset: ∀ {α : Type ?u.21813} {ι : Type ?u.21812} {ι' : Type ?u.21811} [inst : Lattice α] [inst_1 : OrderBot α] {s : Set ι'}
{g : ι' → Finset ι} {f : ι → α},
(Set.PairwiseDisjoint s fun i' => Finset.sup (g i') f) →
(∀ (i : ι'), i ∈ s → Set.PairwiseDisjoint (↑(g i)) f) →
Set.PairwiseDisjoint (Set.iUnion fun i => Set.iUnion fun h => ↑(g i)) fbiUnion_finset hg: ∀ (i' : ι'), i' ∈ s → Set.PairwiseDisjoint (↑(g i')) fhgGoals accomplished! 🐙
#align finset.sup_indep.sup Finset.SupIndep.sup: ∀ {α : Type u_3} {ι : Type u_1} {ι' : Type u_2} [inst : DistribLattice α] [inst_1 : OrderBot α] [inst_2 : DecidableEq ι]
{s : Finset ι'} {g : ι' → Finset ι} {f : ι → α},
(SupIndep s fun i => sup (g i) f) → (∀ (i' : ι'), i' ∈ s → SupIndep (g i') f) → SupIndep (sup s g) fFinset.SupIndep.sup

/-- Bind operation for `SupIndep`. -/
theorem SupIndep.biUnion: ∀ {α : Type u_3} {ι : Type u_1} {ι' : Type u_2} [inst : DistribLattice α] [inst_1 : OrderBot α] [inst_2 : DecidableEq ι]
{s : Finset ι'} {g : ι' → Finset ι} {f : ι → α},
(SupIndep s fun i => Finset.sup (g i) f) → (∀ (i' : ι'), i' ∈ s → SupIndep (g i') f) → SupIndep (Finset.biUnion s g) fSupIndep.biUnion [DecidableEq: Sort ?u.22414 → Sort (max1?u.22414)DecidableEq ι: Type ?u.22027ι] {s: Finset ι's : Finset: Type ?u.22423 → Type ?u.22423Finset ι': Type ?u.22030ι'} {g: ι' → Finset ιg : ι': Type ?u.22030ι' → Finset: Type ?u.22428 → Type ?u.22428Finset ι: Type ?u.22027ι} {f: ι → αf : ι: Type ?u.22027ι → α: Type ?u.22021α}
(hs: SupIndep s fun i => Finset.sup (g i) fhs : s: Finset ι's.SupIndep: {α : Type ?u.22436} → {ι : Type ?u.22435} → [inst : Lattice α] → [inst : OrderBot α] → Finset ι → (ι → α) → PropSupIndep fun i: ?m.22500i => (g: ι' → Finset ιg i: ?m.22500i).sup: {α : Type ?u.22503} → {β : Type ?u.22502} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → αsup f: ι → αf) (hg: ∀ (i' : ι'), i' ∈ s → SupIndep (g i') fhg : ∀ i': ?m.22752i' ∈ s: Finset ι's, (g: ι' → Finset ιg i': ?m.22752i').SupIndep: {α : Type ?u.22786} → {ι : Type ?u.22785} → [inst : Lattice α] → [inst : OrderBot α] → Finset ι → (ι → α) → PropSupIndep f: ι → αf) :
(s: Finset ι's.biUnion: {α : Type ?u.22856} → {β : Type ?u.22855} → [inst : DecidableEq β] → Finset α → (α → Finset β) → Finset βbiUnion g: ι' → Finset ιg).SupIndep: {α : Type ?u.22910} → {ι : Type ?u.22909} → [inst : Lattice α] → [inst : OrderBot α] → Finset ι → (ι → α) → PropSupIndep f: ι → αf := byGoals accomplished! 🐙
α: Type u_3β: Type ?u.22024ι: Type u_1ι': Type u_2inst✝²: DistribLattice αinst✝¹: OrderBot αs✝: Finset ιf✝: ι → αinst✝: DecidableEq ιs: Finset ι'g: ι' → Finset ιf: ι → αhs: SupIndep s fun i => Finset.sup (g i) fhg: ∀ (i' : ι'), i' ∈ s → SupIndep (g i') fSupIndep (Finset.biUnion s g) frw [α: Type u_3β: Type ?u.22024ι: Type u_1ι': Type u_2inst✝²: DistribLattice αinst✝¹: OrderBot αs✝: Finset ιf✝: ι → αinst✝: DecidableEq ιs: Finset ι'g: ι' → Finset ιf: ι → αhs: SupIndep s fun i => Finset.sup (g i) fhg: ∀ (i' : ι'), i' ∈ s → SupIndep (g i') fSupIndep (Finset.biUnion s g) f← sup_eq_biUnion: ∀ {α : Type ?u.22996} {β : Type ?u.22997} [inst : DecidableEq β] (s : Finset α) (t : α → Finset β),
Finset.sup s t = Finset.biUnion s tsup_eq_biUnionα: Type u_3β: Type ?u.22024ι: Type u_1ι': Type u_2inst✝²: DistribLattice αinst✝¹: OrderBot αs✝: Finset ιf✝: ι → αinst✝: DecidableEq ιs: Finset ι'g: ι' → Finset ιf: ι → αhs: SupIndep s fun i => Finset.sup (g i) fhg: ∀ (i' : ι'), i' ∈ s → SupIndep (g i') fSupIndep (Finset.sup s g) f]α: Type u_3β: Type ?u.22024ι: Type u_1ι': Type u_2inst✝²: DistribLattice αinst✝¹: OrderBot αs✝: Finset ιf✝: ι → αinst✝: DecidableEq ιs: Finset ι'g: ι' → Finset ιf: ι → αhs: SupIndep s fun i => Finset.sup (g i) fhg: ∀ (i' : ι'), i' ∈ s → SupIndep (g i') fSupIndep (Finset.sup s g) f
α: Type u_3β: Type ?u.22024ι: Type u_1ι': Type u_2inst✝²: DistribLattice αinst✝¹: OrderBot αs✝: Finset ιf✝: ι → αinst✝: DecidableEq ιs: Finset ι'g: ι' → Finset ιf: ι → αhs: SupIndep s fun i => Finset.sup (g i) fhg: ∀ (i' : ι'), i' ∈ s → SupIndep (g i') fSupIndep (Finset.biUnion s g) fexact hs: SupIndep s fun i => Finset.sup (g i) fhs.sup: ∀ {α : Type ?u.23205} {ι : Type ?u.23203} {ι' : Type ?u.23204} [inst : DistribLattice α] [inst_1 : OrderBot α]
[inst_2 : DecidableEq ι] {s : Finset ι'} {g : ι' → Finset ι} {f : ι → α},
(SupIndep s fun i => Finset.sup (g i) f) → (∀ (i' : ι'), i' ∈ s → SupIndep (g i') f) → SupIndep (Finset.sup s g) fsup hg: ∀ (i' : ι'), i' ∈ s → SupIndep (g i') fhgGoals accomplished! 🐙
#align finset.sup_indep.bUnion Finset.SupIndep.biUnion: ∀ {α : Type u_3} {ι : Type u_1} {ι' : Type u_2} [inst : DistribLattice α] [inst_1 : OrderBot α] [inst_2 : DecidableEq ι]
{s : Finset ι'} {g : ι' → Finset ι} {f : ι → α},
(SupIndep s fun i => sup (g i) f) → (∀ (i' : ι'), i' ∈ s → SupIndep (g i') f) → SupIndep (Finset.biUnion s g) fFinset.SupIndep.biUnion

end DistribLattice

end Finset

/-! ### On complete lattices via `sSup` -/

namespace CompleteLattice

variable [CompleteLattice: Type ?u.26923 → Type ?u.26923CompleteLattice α: Type ?u.23352α]

open Set Function

/-- An independent set of elements in a complete lattice is one in which every element is disjoint
from the `Sup` of the rest. -/
def SetIndependent: {α : Type u_1} → [inst : CompleteLattice α] → Set α → PropSetIndependent (s: Set αs : Set: Type ?u.23382 → Type ?u.23382Set α: Type ?u.23367α) : Prop: TypeProp :=
∀ ⦃a: ?m.23388a⦄, a: ?m.23388a ∈ s: Set αs → Disjoint: {α : Type ?u.23422} → [inst : PartialOrder α] → [inst : OrderBot α] → α → α → PropDisjoint a: ?m.23388a (sSup: {α : Type ?u.23497} → [self : SupSet α] → Set α → αsSup (s: Set αs \ {a: ?m.23388a}))
#align complete_lattice.set_independent CompleteLattice.SetIndependent: {α : Type u_1} → [inst : CompleteLattice α] → Set α → PropCompleteLattice.SetIndependent

variable {s: Set αs : Set: Type ?u.50592 → Type ?u.50592Set α: Type ?u.50577α} (hs: SetIndependent shs : SetIndependent: {α : Type ?u.36305} → [inst : CompleteLattice α] → Set α → PropSetIndependent s: Set αs)

@[simp]
theorem setIndependent_empty: SetIndependent ∅setIndependent_empty : SetIndependent: {α : Type ?u.23748} → [inst : CompleteLattice α] → Set α → PropSetIndependent (∅: ?m.23764∅ : Set: Type ?u.23762 → Type ?u.23762Set α: Type ?u.23706α) := fun x: ?m.23817x hx: ?m.23820hx =>
(Set.not_mem_empty: ∀ {α : Type ?u.23822} (x : α), ¬x ∈ ∅Set.not_mem_empty x: ?m.23817x hx: ?m.23820hx).elim: ∀ {C : Sort ?u.23824}, False → Celim
#align complete_lattice.set_independent_empty CompleteLattice.setIndependent_empty: ∀ {α : Type u_1} [inst : CompleteLattice α], SetIndependent ∅CompleteLattice.setIndependent_empty

theorem SetIndependent.mono: ∀ {t : Set α}, t ⊆ s → SetIndependent tSetIndependent.mono {t: Set αt : Set: Type ?u.23891 → Type ?u.23891Set α: Type ?u.23849α} (hst: t ⊆ shst : t: Set αt ⊆ s: Set αs) : SetIndependent: {α : Type ?u.23915} → [inst : CompleteLattice α] → Set α → PropSetIndependent t: Set αt := fun _: ?m.23942_ ha: ?m.23945ha =>
(hs: SetIndependent shs (hst: t ⊆ shst ha: ?m.23945ha)).mono_right: ∀ {α : Type ?u.23954} [inst : PartialOrder α] [inst_1 : OrderBot α] {a b c : α}, b ≤ c → Disjoint a c → Disjoint a bmono_right (sSup_le_sSup: ∀ {α : Type ?u.24054} [inst : CompleteSemilatticeSup α] {s t : Set α}, s ⊆ t → sSup s ≤ sSup tsSup_le_sSup (diff_subset_diff_left: ∀ {α : Type ?u.24099} {s₁ s₂ t : Set α}, s₁ ⊆ s₂ → s₁ \ t ⊆ s₂ \ tdiff_subset_diff_left hst: t ⊆ shst))
#align complete_lattice.set_independent.mono CompleteLattice.SetIndependent.mono: ∀ {α : Type u_1} [inst : CompleteLattice α] {s : Set α}, SetIndependent s → ∀ {t : Set α}, t ⊆ s → SetIndependent tCompleteLattice.SetIndependent.mono

/-- If the elements of a set are independent, then any pair within that set is disjoint. -/
theorem SetIndependent.pairwiseDisjoint: PairwiseDisjoint s idSetIndependent.pairwiseDisjoint : s: Set αs.PairwiseDisjoint: {α : Type ?u.24246} → {ι : Type ?u.24245} → [inst : PartialOrder α] → [inst : OrderBot α] → Set ι → (ι → α) → PropPairwiseDisjoint id: {α : Sort ?u.24329} → α → αid := fun _: ?m.24409_ hx: ?m.24412hx y: ?m.24415y hy: ?m.24418hy h: ?m.24421h =>
disjoint_sSup_right: ∀ {α : Type ?u.24423} [inst : CompleteLattice α] {a : Set α} {b : α},
Disjoint b (sSup a) → ∀ {i : α}, i ∈ a → Disjoint b idisjoint_sSup_right (hs: SetIndependent shs hx: ?m.24412hx) ((mem_diff: ∀ {α : Type ?u.24467} {s t : Set α} (x : α), x ∈ s \ t ↔ x ∈ s ∧ ¬x ∈ tmem_diff y: ?m.24415y).mpr: ∀ {a b : Prop}, (a ↔ b) → b → ampr ⟨hy: ?m.24418hy, h: ?m.24421h.symm: ∀ {α : Sort ?u.24487} {a b : α}, a ≠ b → b ≠ asymm⟩)
#align complete_lattice.set_independent.pairwise_disjoint CompleteLattice.SetIndependent.pairwiseDisjoint: ∀ {α : Type u_1} [inst : CompleteLattice α] {s : Set α}, SetIndependent s → PairwiseDisjoint s idCompleteLattice.SetIndependent.pairwiseDisjoint

theorem setIndependent_pair: ∀ {α : Type u_1} [inst : CompleteLattice α] {a b : α}, a ≠ b → (SetIndependent {a, b} ↔ Disjoint a b)setIndependent_pair {a: αa b: αb : α: Type ?u.24525α} (hab: a ≠ bhab : a: αa ≠ b: αb) :
SetIndependent: {α : Type ?u.24575} → [inst : CompleteLattice α] → Set α → PropSetIndependent ({a: αa, b: αb} : Set: Type ?u.24579 → Type ?u.24579Set α: Type ?u.24525α) ↔ Disjoint: {α : Type ?u.24636} → [inst : PartialOrder α] → [inst : OrderBot α] → α → α → PropDisjoint a: αa b: αb := byGoals accomplished! 🐙
α: Type u_1β: Type ?u.24528ι: Type ?u.24531ι': Type ?u.24534inst✝: CompleteLattice αs: Set αhs: SetIndependent sa, b: αhab: a ≠ bSetIndependent {a, b} ↔ Disjoint a bconstructorα: Type u_1β: Type ?u.24528ι: Type ?u.24531ι': Type ?u.24534inst✝: CompleteLattice αs: Set αhs: SetIndependent sa, b: αhab: a ≠ bmpSetIndependent {a, b} → Disjoint a bα: Type u_1β: Type ?u.24528ι: Type ?u.24531ι': Type ?u.24534inst✝: CompleteLattice αs: Set αhs: SetIndependent sa, b: αhab: a ≠ bmprDisjoint a b → SetIndependent {a, b}
α: Type u_1β: Type ?u.24528ι: Type ?u.24531ι': Type ?u.24534inst✝: CompleteLattice αs: Set αhs: SetIndependent sa, b: αhab: a ≠ bSetIndependent {a, b} ↔ Disjoint a b·α: Type u_1β: Type ?u.24528ι: Type ?u.24531ι': Type ?u.24534inst✝: CompleteLattice αs: Set αhs: SetIndependent sa, b: αhab: a ≠ bmpSetIndependent {a, b} → Disjoint a b α: Type u_1β: Type ?u.24528ι: Type ?u.24531ι': Type ?u.24534inst✝: CompleteLattice αs: Set αhs: SetIndependent sa, b: αhab: a ≠ bmpSetIndependent {a, b} → Disjoint a bα: Type u_1β: Type ?u.24528ι: Type ?u.24531ι': Type ?u.24534inst✝: CompleteLattice αs: Set αhs: SetIndependent sa, b: αhab: a ≠ bmprDisjoint a b → SetIndependent {a, b}intro h: ?ahα: Type u_1β: Type ?u.24528ι: Type ?u.24531ι': Type ?u.24534inst✝: CompleteLattice αs: Set αhs: SetIndependent sa, b: αhab: a ≠ bh: SetIndependent {a, b}mpDisjoint a b
α: Type u_1β: Type ?u.24528ι: Type ?u.24531ι': Type ?u.24534inst✝: CompleteLattice αs: Set αhs: SetIndependent sa, b: αhab: a ≠ bmpSetIndependent {a, b} → Disjoint a bexact h: ?ah.pairwiseDisjoint: ∀ {α : Type ?u.24730} [inst : CompleteLattice α] {s : Set α}, SetIndependent s → PairwiseDisjoint s idpairwiseDisjoint (mem_insert: ∀ {α : Type ?u.24753} (x : α) (s : Set α), x ∈ insert x smem_insert _: ?m.24754_ _: Set ?m.24754_) (mem_insert_of_mem: ∀ {α : Type ?u.24781} {x : α} {s : Set α} (y : α), x ∈ s → x ∈ insert y smem_insert_of_mem _: ?m.24782_ (mem_singleton: ∀ {α : Type ?u.24786} (a : α), a ∈ {a}mem_singleton _: ?m.24787_)) hab: a ≠ bhabGoals accomplished! 🐙
α: Type u_1β: Type ?u.24528ι: Type ?u.24531ι': Type ?u.24534inst✝: CompleteLattice αs: Set αhs: SetIndependent sa, b: αhab: a ≠ bSetIndependent {a, b} ↔ Disjoint a b·α: Type u_1β: Type ?u.24528ι: Type ?u.24531ι': Type ?u.24534inst✝: CompleteLattice αs: Set αhs: SetIndependent sa, b: αhab: a ≠ bmprDisjoint a b → SetIndependent {a, b} α: Type u_1β: Type ?u.24528ι: Type ?u.24531ι': Type ?u.24534inst✝: CompleteLattice αs: Set αhs: SetIndependent sa, b: αhab: a ≠ bmprDisjoint a b → SetIndependent {a, b}rintro h: ?bh c: αc ((rfl : c = a) | (rfl : c = b)): c ∈ {a, b}((rfl : c = a) | (rfl : c = b): c ∈ {a, b}(rfl: c = arflrfl : c = a: c = a : c: αcrfl : c = a: c = a = a: αa(rfl : c = a) | (rfl : c = b): c ∈ {a, b}) | (rfl: c = brflrfl : c = b: c ∈ {b} : c: αcrfl : c = b: c ∈ {b} = b: αb(rfl : c = a) | (rfl : c = b): c ∈ {a, b})((rfl : c = a) | (rfl : c = b)): c ∈ {a, b})α: Type u_1β: Type ?u.24528ι: Type ?u.24531ι': Type ?u.24534inst✝: CompleteLattice αs: Set αhs: SetIndependent sb, c: αhab: c ≠ bh: Disjoint c bmpr.inlDisjoint c (sSup ({c, b} \ {c}))α: Type u_1β: Type ?u.24528ι: Type ?u.24531ι': Type ?u.24534inst✝: CompleteLattice αs: Set αhs: SetIndependent sa, c: αhab: a ≠ ch: Disjoint a cmpr.inrDisjoint c (sSup ({a, c} \ {c}))
α: Type u_1β: Type ?u.24528ι: Type ?u.24531ι': Type ?u.24534inst✝: CompleteLattice αs: Set αhs: SetIndependent sa, b: αhab: a ≠ bmprDisjoint a b → SetIndependent {a, b}·α: Type u_1β: Type ?u.24528ι: Type ?u.24531ι': Type ?u.24534inst✝: CompleteLattice αs: Set αhs: SetIndependent sb, c: αhab: c ≠ bh: Disjoint c bmpr.inlDisjoint c (sSup ({c, b} \ {c})) α: Type u_1β: Type ?u.24528ι: Type ?u.24531ι': Type ?u.24534inst✝: CompleteLattice αs: Set αhs: SetIndependent sb, c: αhab: c ≠ bh: Disjoint c bmpr.inlDisjoint c (sSup ({c, b} \ {c}))α: Type u_1β: Type ?u.24528ι: Type ?u.24531ι': Type ?u.24534inst✝: CompleteLattice αs: Set αhs: SetIndependent sa, c: αhab: a ≠ ch: Disjoint a cmpr.inrDisjoint c (sSup ({a, c} \ {c}))convert h: Disjoint c bh using 1α: Type u_1β: Type ?u.24528ι: Type ?u.24531ι': Type ?u.24534inst✝: CompleteLattice αs: Set αhs: SetIndependent sb, c: αhab: c ≠ bh: Disjoint c bh.e'_5sSup ({c, b} \ {c}) = b
α: Type u_1β: Type ?u.24528ι: Type ?u.24531ι': Type ?u.24534inst✝: CompleteLattice αs: Set αhs: SetIndependent sb, c: αhab: c ≠ bh: Disjoint c bmpr.inlDisjoint c (sSup ({c, b} \ {c}))simp [hab: c ≠ bhab, sSup_singleton: ∀ {α : Type ?u.25195} [inst : CompleteSemilatticeSup α] {a : α}, sSup {a} = asSup_singleton]Goals accomplished! 🐙
α: Type u_1β: Type ?u.24528ι: Type ?u.24531ι': Type ?u.24534inst✝: CompleteLattice αs: Set αhs: SetIndependent sa, b: αhab: a ≠ bmprDisjoint a b → SetIndependent {a, b}·α: Type u_1β: Type ?u.24528ι: Type ?u.24531ι': Type ?u.24534inst✝: CompleteLattice αs: Set αhs: SetIndependent sa, c: αhab: a ≠ ch: Disjoint a cmpr.inrDisjoint c (sSup ({a, c} \ {c})) α: Type u_1β: Type ?u.24528ι: Type ?u.24531ι': Type ?u.24534inst✝: CompleteLattice αs: Set αhs: SetIndependent sa, c: αhab: a ≠ ch: Disjoint a cmpr.inrDisjoint c (sSup ({a, c} \ {c}))convert h: Disjoint a ch.symm: ∀ {α : Type ?u.25691} [inst : PartialOrder α] [inst_1 : OrderBot α] ⦃a b : α⦄, Disjoint a b → Disjoint b asymm using 1α: Type u_1β: Type ?u.24528ι: Type ?u.24531ι': Type ?u.24534inst✝: CompleteLattice αs: Set αhs: SetIndependent sa, c: αhab: a ≠ ch: Disjoint a ch.e'_5sSup ({a, c} \ {c}) = a
α: Type u_1β: Type ?u.24528ι: Type ?u.24531ι': Type ?u.24534inst✝: CompleteLattice αs: Set αhs: SetIndependent sa, c: αhab: a ≠ ch: Disjoint a cmpr.inrDisjoint c (sSup ({a, c} \ {c}))simp [hab: a ≠ chab, sSup_singleton: ∀ {α : Type ?u.26033} [inst : CompleteSemilatticeSup α] {a : α}, sSup {a} = asSup_singleton]Goals accomplished! 🐙
#align complete_lattice.set_independent_pair CompleteLattice.setIndependent_pair: ∀ {α : Type u_1} [inst : CompleteLattice α] {a b : α}, a ≠ b → (SetIndependent {a, b} ↔ Disjoint a b)CompleteLattice.setIndependent_pair

/-- If the elements of a set are independent, then any element is disjoint from the `sSup` of some
subset of the rest. -/
theorem SetIndependent.disjoint_sSup: ∀ {x : α} {y : Set α}, x ∈ s → y ⊆ s → ¬x ∈ y → Disjoint x (sSup y)SetIndependent.disjoint_sSup {x: αx : α: Type ?u.26448α} {y: Set αy : Set: Type ?u.26492 → Type ?u.26492Set α: Type ?u.26448α} (hx: x ∈ shx : x: αx ∈ s: Set αs) (hy: y ⊆ shy : y: Set αy ⊆ s: Set αs) (hxy: ¬x ∈ yhxy : x: αx ∉ y: Set αy) :
Disjoint: {α : Type ?u.26552} → [inst : PartialOrder α] → [inst : OrderBot α] → α → α → PropDisjoint x: αx (sSup: {α : Type ?u.26627} → [self : SupSet α] → Set α → αsSup y: Set αy) := byGoals accomplished! 🐙
α: Type u_1β: Type ?u.26451ι: Type ?u.26454ι': Type ?u.26457inst✝: CompleteLattice αs: Set αhs: SetIndependent sx: αy: Set αhx: x ∈ shy: y ⊆ shxy: ¬x ∈ yDisjoint x (sSup y)have := (hs: SetIndependent shs.mono: ∀ {α : Type ?u.26744} [inst : CompleteLattice α] {s : Set α}, SetIndependent s → ∀ {t : Set α}, t ⊆ s → SetIndependent tmono <| insert_subset: ∀ {α : Type ?u.26766} {a : α} {s t : Set α}, insert a s ⊆ t ↔ a ∈ t ∧ s ⊆ tinsert_subset.mpr: ∀ {a b : Prop}, (a ↔ b) → b → ampr ⟨hx: x ∈ shx, hy: y ⊆ shy⟩) (mem_insert: ∀ {α : Type ?u.26803} (x : α) (s : Set α), x ∈ insert x smem_insert x: αx _: Set ?m.26804_)α: Type u_1β: Type ?u.26451ι: Type ?u.26454ι': Type ?u.26457inst✝: CompleteLattice αs: Set αhs: SetIndependent sx: αy: Set αhx: x ∈ shy: y ⊆ shxy: ¬x ∈ ythis: Disjoint x (sSup (insert x y \ {x}))Disjoint x (sSup y)
α: Type u_1β: Type ?u.26451ι: Type ?u.26454ι': Type ?u.26457inst✝: CompleteLattice αs: Set αhs: SetIndependent sx: αy: Set αhx: x ∈ shy: y ⊆ shxy: ¬x ∈ yDisjoint x (sSup y)rw [α: Type u_1β: Type ?u.26451ι: Type ?u.26454ι': Type ?u.26457inst✝: CompleteLattice αs: Set αhs: SetIndependent sx: αy: Set αhx: x ∈ shy: y ⊆ shxy: ¬x ∈ ythis: Disjoint x (sSup (insert x y \ {x}))Disjoint x (sSup y)insert_diff_of_mem: ∀ {α : Type ?u.26820} {a : α} {t : Set α} (s : Set α), a ∈ t → insert a s \ t = s \ tinsert_diff_of_mem _: Set ?m.26821_ (mem_singleton: ∀ {α : Type ?u.26825} (a : α), a ∈ {a}mem_singleton _: ?m.26826_),α: Type u_1β: Type ?u.26451ι: Type ?u.26454ι': Type ?u.26457inst✝: CompleteLattice αs: Set αhs: SetIndependent sx: αy: Set αhx: x ∈ shy: y ⊆ shxy: ¬x ∈ ythis: Disjoint x (sSup (y \ {x}))Disjoint x (sSup y) α: Type u_1β: Type ?u.26451ι: Type ?u.26454ι': Type ?u.26457inst✝: CompleteLattice αs: Set αhs: SetIndependent sx: αy: Set αhx: x ∈ shy: y ⊆ shxy: ¬x ∈ ythis: Disjoint x (sSup (insert x y \ {x}))Disjoint x (sSup y)diff_singleton_eq_self: ∀ {α : Type ?u.26869} {a : α} {s : Set α}, ¬a ∈ s → s \ {a} = sdiff_singleton_eq_self hxy: ¬x ∈ yhxyα: Type u_1β: Type ?u.26451ι: Type ?u.26454ι': Type ?u.26457inst✝: CompleteLattice αs: Set αhs: SetIndependent sx: αy: Set αhx: x ∈ shy: y ⊆ shxy: ¬x ∈ ythis: Disjoint x (sSup y)Disjoint x (sSup y)]α: Type u_1β: Type ?u.26451ι: Type ?u.26454ι': Type ?u.26457inst✝: CompleteLattice αs: Set αhs: SetIndependent sx: αy: Set αhx: x ∈ shy: y ⊆ shxy: ¬x ∈ ythis: Disjoint x (sSup y)Disjoint x (sSup y) at this: Disjoint x (sSup (y \ {x}))thisα: Type u_1β: Type ?u.26451ι: Type ?u.26454ι': Type ?u.26457inst✝: CompleteLattice αs: Set αhs: SetIndependent sx: αy: Set αhx: x ∈ shy: y ⊆ shxy: ¬x ∈ ythis: Disjoint x (sSup y)Disjoint x (sSup y)
α: Type u_1β: Type ?u.26451ι: Type ?u.26454ι': Type ?u.26457inst✝: CompleteLattice αs: Set αhs: SetIndependent sx: αy: Set αhx: x ∈ shy: y ⊆ shxy: ¬x ∈ yDisjoint x (sSup y)exact this: Disjoint x (sSup y)thisGoals accomplished! 🐙
#align complete_lattice.set_independent.disjoint_Sup CompleteLattice.SetIndependent.disjoint_sSup: ∀ {α : Type u_1} [inst : CompleteLattice α] {s : Set α},
SetIndependent s → ∀ {x : α} {y : Set α}, x ∈ s → y ⊆ s → ¬x ∈ y → Disjoint x (sSup y)CompleteLattice.SetIndependent.disjoint_sSup

/-- An independent indexed family of elements in a complete lattice is one in which every element
is disjoint from the `iSup` of the rest.

Example: an indexed family of non-zero elements in a
vector space is linearly independent iff the indexed family of subspaces they generate is
independent in this sense.

Example: an indexed family of submodules of a module is independent in this sense if
and only the natural map from the direct sum of the submodules to the module is injective. -/
-- Porting note: needed to use `_H`
def Independent: {ι : Sort ?u.26953} → {α : Type ?u.26956} → [inst : CompleteLattice α] → (ι → α) → PropIndependent {ι: Sort ?u.26953ι : Sort _: Type ?u.26953SortSort _: Type ?u.26953 _} {α: Type ?u.26956α : Type _: Type (?u.26956+1)Type _} [CompleteLattice: Type ?u.26959 → Type ?u.26959CompleteLattice α: Type ?u.26956α] (t: ι → αt : ι: Sort ?u.26953ι → α: Type ?u.26956α) : ```