case tfae_1_to_2
ι : Sort ?u.77139
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
⊢ (WellFounded fun x x_1 => x > x_1) → IsSupFiniteCompact α

ι : Sort ?u.77139
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
tfae_1_to_2 : (WellFounded fun x x_1 => x > x_1) → IsSupFiniteCompact α
⊢ TFAE [WellFounded fun x x_1 => x > x_1, IsSupFiniteCompact α, IsSupClosedCompact α, ∀ (k : α), IsCompactElement k]
ι : Sort ?u.77139
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
⊢ TFAE [WellFounded fun x x_1 => x > x_1, IsSupFiniteCompact α, IsSupClosedCompact α, ∀ (k : α), IsCompactElement k]
tfae_have 1 → 2
case tfae_2_to_3
ι : Sort ?u.77139
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
tfae_1_to_2 : (WellFounded fun x x_1 => x > x_1) → IsSupFiniteCompact α
⊢ IsSupFiniteCompact α → IsSupClosedCompact α

ι : Sort ?u.77139
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
tfae_1_to_2 : (WellFounded fun x x_1 => x > x_1) → IsSupFiniteCompact α
tfae_2_to_3 : IsSupFiniteCompact α → IsSupClosedCompact α
⊢ TFAE [WellFounded fun x x_1 => x > x_1, IsSupFiniteCompact α, IsSupClosedCompact α, ∀ (k : α), IsCompactElement k]
ι : Sort ?u.77139
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
tfae_1_to_2 : (WellFounded fun x x_1 => x > x_1) → IsSupFiniteCompact α
⊢ TFAE [WellFounded fun x x_1 => x > x_1, IsSupFiniteCompact α, IsSupClosedCompact α, ∀ (k : α), IsCompactElement k]
tfae_have 2 → 3
case tfae_3_to_1
ι : Sort ?u.77139
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
tfae_1_to_2 : (WellFounded fun x x_1 => x > x_1) → IsSupFiniteCompact α
tfae_2_to_3 : IsSupFiniteCompact α → IsSupClosedCompact α
⊢ IsSupClosedCompact α → WellFounded fun x x_1 => x > x_1

ι : Sort ?u.77139
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
tfae_1_to_2 : (WellFounded fun x x_1 => x > x_1) → IsSupFiniteCompact α
tfae_2_to_3 : IsSupFiniteCompact α → IsSupClosedCompact α
tfae_3_to_1 : IsSupClosedCompact α → WellFounded fun x x_1 => x > x_1
⊢ TFAE [WellFounded fun x x_1 => x > x_1, IsSupFiniteCompact α, IsSupClosedCompact α, ∀ (k : α), IsCompactElement k]
ι : Sort ?u.77139
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
tfae_1_to_2 : (WellFounded fun x x_1 => x > x_1) → IsSupFiniteCompact α
tfae_2_to_3 : IsSupFiniteCompact α → IsSupClosedCompact α
⊢ TFAE [WellFounded fun x x_1 => x > x_1, IsSupFiniteCompact α, IsSupClosedCompact α, ∀ (k : α), IsCompactElement k]
tfae_have 3 → 1
case tfae_2_iff_4
ι : Sort ?u.77139
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
tfae_1_to_2 : (WellFounded fun x x_1 => x > x_1) → IsSupFiniteCompact α
tfae_2_to_3 : IsSupFiniteCompact α → IsSupClosedCompact α
tfae_3_to_1 : IsSupClosedCompact α → WellFounded fun x x_1 => x > x_1
⊢ IsSupFiniteCompact α ↔ ∀ (k : α), IsCompactElement k

ι : Sort ?u.77139
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
tfae_1_to_2 : (WellFounded fun x x_1 => x > x_1) → IsSupFiniteCompact α
tfae_2_to_3 : IsSupFiniteCompact α → IsSupClosedCompact α
tfae_3_to_1 : IsSupClosedCompact α → WellFounded fun x x_1 => x > x_1
tfae_2_iff_4 : IsSupFiniteCompact α ↔ ∀ (k : α), IsCompactElement k
⊢ TFAE [WellFounded fun x x_1 => x > x_1, IsSupFiniteCompact α, IsSupClosedCompact α, ∀ (k : α), IsCompactElement k]
ι : Sort ?u.77139
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
tfae_1_to_2 : (WellFounded fun x x_1 => x > x_1) → IsSupFiniteCompact α
tfae_2_to_3 : IsSupFiniteCompact α → IsSupClosedCompact α
tfae_3_to_1 : IsSupClosedCompact α → WellFounded fun x x_1 => x > x_1
⊢ TFAE [WellFounded fun x x_1 => x > x_1, IsSupFiniteCompact α, IsSupClosedCompact α, ∀ (k : α), IsCompactElement k]
tfae_have 2 ↔ 4
no goals
ι : Sort ?u.77139
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
tfae_1_to_2 : (WellFounded fun x x_1 => x > x_1) → IsSupFiniteCompact α
tfae_2_to_3 : IsSupFiniteCompact α → IsSupClosedCompact α
tfae_3_to_1 : IsSupClosedCompact α → WellFounded fun x x_1 => x > x_1
tfae_2_iff_4 : IsSupFiniteCompact α ↔ ∀ (k : α), IsCompactElement k
⊢ TFAE [WellFounded fun x x_1 => x > x_1, IsSupFiniteCompact α, IsSupClosedCompact α, ∀ (k : α), IsCompactElement k]
tfae_finish
no goals
case tfae_1_to_2
ι : Sort ?u.77139
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
⊢ (WellFounded fun x x_1 => x > x_1) → IsSupFiniteCompact α
exact WellFounded.isSupFiniteCompact α
no goals
case tfae_2_to_3
ι : Sort ?u.77139
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
tfae_1_to_2 : (WellFounded fun x x_1 => x > x_1) → IsSupFiniteCompact α
⊢ IsSupFiniteCompact α → IsSupClosedCompact α
exact IsSupFiniteCompact.isSupClosedCompact α
no goals
case tfae_3_to_1
ι : Sort ?u.77139
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
tfae_1_to_2 : (WellFounded fun x x_1 => x > x_1) → IsSupFiniteCompact α
tfae_2_to_3 : IsSupFiniteCompact α → IsSupClosedCompact α
⊢ IsSupClosedCompact α → WellFounded fun x x_1 => x > x_1
exact IsSupClosedCompact.wellFounded α
no goals
case tfae_2_iff_4
ι : Sort ?u.77139
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
tfae_1_to_2 : (WellFounded fun x x_1 => x > x_1) → IsSupFiniteCompact α
tfae_2_to_3 : IsSupFiniteCompact α → IsSupClosedCompact α
tfae_3_to_1 : IsSupClosedCompact α → WellFounded fun x x_1 => x > x_1
⊢ IsSupFiniteCompact α ↔ ∀ (k : α), IsCompactElement k
exact isSupFiniteCompact_iff_all_elements_compact α