case h
ι : Type u_1
α : ι → Type u_2
β : ι → Type ?u.115563
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
hs : i ∈ s
ht : t i = ∅
f : (i : ι) → α i
⊢ f ∈ pi s t ↔ f ∈ ∅
ι : Type u_1
α : ι → Type u_2
β : ι → Type ?u.115563
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
hs : i ∈ s
ht : t i = ∅
⊢ pi s t = ∅
ext f
case h
ι : Type u_1
α : ι → Type u_2
β : ι → Type ?u.115563
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
hs : i ∈ s
ht : t i = ∅
f : (i : ι) → α i
⊢ ∃ x, x ∈ s ∧ ¬f x ∈ t x
case h
ι : Type u_1
α : ι → Type u_2
β : ι → Type ?u.115563
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
hs : i ∈ s
ht : t i = ∅
f : (i : ι) → α i
⊢ f ∈ pi s t ↔ f ∈ ∅
simp only [mem_empty_iff_false, not_forall, iff_false_iff, mem_pi, not_imp]
no goals
case h
ι : Type u_1
α : ι → Type u_2
β : ι → Type ?u.115563
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
hs : i ∈ s
ht : t i = ∅
f : (i : ι) → α i
⊢ ∃ x, x ∈ s ∧ ¬f x ∈ t x
exact ⟨i, hs, by simp [ht]⟩
no goals
ι : Type u_1
α : ι → Type u_2
β : ι → Type ?u.115563
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
hs : i ∈ s
ht : t i = ∅
f : (i : ι) → α i
⊢ ¬f i ∈ t i
simp [ht]