𝕜 : Type ?u.13760
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ v, v ∈ 𝒜 ∧ s ⊆ v ∧ card s = k) ↔ (∃ t, t ∈ 𝒜 ∧ s ⊆ t) ∧ card s = k
𝕜 : Type ?u.13760
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ falling k 𝒜 ↔ (∃ t, t ∈ 𝒜 ∧ s ⊆ t) ∧ card s = k
simp_rw [falling, mem_sup, mem_powersetLen]
no goals
𝕜 : Type ?u.13760
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ v, v ∈ 𝒜 ∧ s ⊆ v ∧ card s = k) ↔ (∃ t, t ∈ 𝒜 ∧ s ⊆ t) ∧ card s = k
aesop