α : Type u_3
β : Type ?u.52493
ι✝ : Type ?u.52496
ι'✝ : Type ?u.52499
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t✝ : ι✝ → α
ht✝ : Independent t✝
ι : Sort u_1
ι' : Sort u_2
t : ι → α
f : ι' → ι
ht : Independent (t ∘ f)
hf : Surjective f
i : ι
⊢ Disjoint (t i) (⨆ (j : ι) (_ : j ≠ i), t j)
α : Type u_3
β : Type ?u.52493
ι✝ : Type ?u.52496
ι'✝ : Type ?u.52499
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t✝ : ι✝ → α
ht✝ : Independent t✝
ι : Sort u_1
ι' : Sort u_2
t : ι → α
f : ι' → ι
ht : Independent (t ∘ f)
hf : Surjective f
⊢ Independent t
intro i
case intro
α : Type u_3
β : Type ?u.52493
ι✝ : Type ?u.52496
ι'✝ : Type ?u.52499
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t✝ : ι✝ → α
ht✝ : Independent t✝
ι : Sort u_1
ι' : Sort u_2
t : ι → α
f : ι' → ι
ht : Independent (t ∘ f)
hf : Surjective f
i' : ι'
⊢ Disjoint (t (f i')) (⨆ (j : ι) (_ : j ≠ f i'), t j)
α : Type u_3
β : Type ?u.52493
ι✝ : Type ?u.52496
ι'✝ : Type ?u.52499
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t✝ : ι✝ → α
ht✝ : Independent t✝
ι : Sort u_1
ι' : Sort u_2
t : ι → α
f : ι' → ι
ht : Independent (t ∘ f)
hf : Surjective f
i : ι
⊢ Disjoint (t i) (⨆ (j : ι) (_ : j ≠ i), t j)
obtain ⟨i', rfl⟩ := hf i
case intro
α : Type u_3
β : Type ?u.52493
ι✝ : Type ?u.52496
ι'✝ : Type ?u.52499
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t✝ : ι✝ → α
ht✝ : Independent t✝
ι : Sort u_1
ι' : Sort u_2
t : ι → α
f : ι' → ι
ht : Independent (t ∘ f)
hf : Surjective f
i' : ι'
⊢ Disjoint (t (f i')) (⨆ (x : ι') (_ : f x ≠ f i'), t (f x))
case intro
α : Type u_3
β : Type ?u.52493
ι✝ : Type ?u.52496
ι'✝ : Type ?u.52499
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t✝ : ι✝ → α
ht✝ : Independent t✝
ι : Sort u_1
ι' : Sort u_2
t : ι → α
f : ι' → ι
ht : Independent (t ∘ f)
hf : Surjective f
i' : ι'
⊢ Disjoint (t (f i')) (⨆ (j : ι) (_ : j ≠ f i'), t j)
rw [← hf.iSup_comp]
no goals
case intro
α : Type u_3
β : Type ?u.52493
ι✝ : Type ?u.52496
ι'✝ : Type ?u.52499
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t✝ : ι✝ → α
ht✝ : Independent t✝
ι : Sort u_1
ι' : Sort u_2
t : ι → α
f : ι' → ι
ht : Independent (t ∘ f)
hf : Surjective f
i' : ι'
⊢ Disjoint (t (f i')) (⨆ (x : ι') (_ : f x ≠ f i'), t (f x))
exact (ht i').mono_right (biSup_mono fun j' hij => mt (congr_arg f) hij)