α : Type u_1
β : Type ?u.26451
ι : Type ?u.26454
ι' : Type ?u.26457
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
x : α
y : Set α
hx : x ∈ s
hy : y ⊆ s
hxy : ¬x ∈ y
this : Disjoint x (sSup (insert x y \ {x}))
⊢ Disjoint x (sSup y)
α : Type u_1
β : Type ?u.26451
ι : Type ?u.26454
ι' : Type ?u.26457
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
x : α
y : Set α
hx : x ∈ s
hy : y ⊆ s
hxy : ¬x ∈ y
⊢ Disjoint x (sSup y)
have := (hs.mono <| insert_subset.mpr ⟨hx, hy⟩) (mem_insert x _)
α : Type u_1
β : Type ?u.26451
ι : Type ?u.26454
ι' : Type ?u.26457
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
x : α
y : Set α
hx : x ∈ s
hy : y ⊆ s
hxy : ¬x ∈ y
this : Disjoint x (sSup y)
⊢ Disjoint x (sSup y)
α : Type u_1
β : Type ?u.26451
ι : Type ?u.26454
ι' : Type ?u.26457
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
x : α
y : Set α
hx : x ∈ s
hy : y ⊆ s
hxy : ¬x ∈ y
this : Disjoint x (sSup (insert x y \ {x}))
⊢ Disjoint x (sSup y)
rw [insert_diff_of_mem _ (mem_singleton _), diff_singleton_eq_self hxy] at this
no goals
α : Type u_1
β : Type ?u.26451
ι : Type ?u.26454
ι' : Type ?u.26457
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
x : α
y : Set α
hx : x ∈ s
hy : y ⊆ s
hxy : ¬x ∈ y
this : Disjoint x (sSup y)
⊢ Disjoint x (sSup y)
exact this