α✝ : Type ?u.201468
β✝ : Type ?u.201471
β₂ : Type ?u.201474
γ : Type ?u.201477
ι : Sort ?u.201480
ι' : Sort ?u.201483
κ : ι → Sort ?u.201488
κ' : ι' → Sort ?u.201493
α : Type u_1
β : Type u_2
s : Set (α → β → Prop)
a : α
b : β
⊢ iSup (fun f => ↑f a) b ↔ ∃ r, r ∈ s ∧ r a b
α✝ : Type ?u.201468
β✝ : Type ?u.201471
β₂ : Type ?u.201474
γ : Type ?u.201477
ι : Sort ?u.201480
ι' : Sort ?u.201483
κ : ι → Sort ?u.201488
κ' : ι' → Sort ?u.201493
α : Type u_1
β : Type u_2
s : Set (α → β → Prop)
a : α
b : β
⊢ sSup s a b ↔ ∃ r, r ∈ s ∧ r a b
rw [sSup_apply]
no goals
α✝ : Type ?u.201468
β✝ : Type ?u.201471
β₂ : Type ?u.201474
γ : Type ?u.201477
ι : Sort ?u.201480
ι' : Sort ?u.201483
κ : ι → Sort ?u.201488
κ' : ι' → Sort ?u.201493
α : Type u_1
β : Type u_2
s : Set (α → β → Prop)
a : α
b : β
⊢ iSup (fun f => ↑f a) b ↔ ∃ r, r ∈ s ∧ r a b
simp [← eq_iff_iff]