case mp
α : Type u_1
β : Type ?u.92
γ : Type ?u.95
ι : Type u_2
ι' : Type ?u.101
r p q : α → α → Prop
f✝ g : ι → α
s t u : Set α
a b : α
f : ι → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
⊢ Set.Pairwise (⋃ (n : ι), f n) r → ∀ (n : ι), Set.Pairwise (f n) r

case mpr
α : Type u_1
β : Type ?u.92
γ : Type ?u.95
ι : Type u_2
ι' : Type ?u.101
r p q : α → α → Prop
f✝ g : ι → α
s t u : Set α
a b : α
f : ι → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
⊢ (∀ (n : ι), Set.Pairwise (f n) r) → Set.Pairwise (⋃ (n : ι), f n) r
α : Type u_1
β : Type ?u.92
γ : Type ?u.95
ι : Type u_2
ι' : Type ?u.101
r p q : α → α → Prop
f✝ g : ι → α
s t u : Set α
a b : α
f : ι → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
⊢ Set.Pairwise (⋃ (n : ι), f n) r ↔ ∀ (n : ι), Set.Pairwise (f n) r
constructor
case mp
α : Type u_1
β : Type ?u.92
γ : Type ?u.95
ι : Type u_2
ι' : Type ?u.101
r p q : α → α → Prop
f✝ g : ι → α
s t u : Set α
a b : α
f : ι → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
H : Set.Pairwise (⋃ (n : ι), f n) r
n : ι
⊢ Set.Pairwise (f n) r
case mp
α : Type u_1
β : Type ?u.92
γ : Type ?u.95
ι : Type u_2
ι' : Type ?u.101
r p q : α → α → Prop
f✝ g : ι → α
s t u : Set α
a b : α
f : ι → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
⊢ Set.Pairwise (⋃ (n : ι), f n) r → ∀ (n : ι), Set.Pairwise (f n) r
intro H n
no goals
case mp
α : Type u_1
β : Type ?u.92
γ : Type ?u.95
ι : Type u_2
ι' : Type ?u.101
r p q : α → α → Prop
f✝ g : ι → α
s t u : Set α
a b : α
f : ι → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
H : Set.Pairwise (⋃ (n : ι), f n) r
n : ι
⊢ Set.Pairwise (f n) r
exact Pairwise.mono (subset_iUnion _ _) H
case mpr
α : Type u_1
β : Type ?u.92
γ : Type ?u.95
ι : Type u_2
ι' : Type ?u.101
r p q : α → α → Prop
f✝ g : ι → α
s t u : Set α
a b : α
f : ι → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
H : ∀ (n : ι), Set.Pairwise (f n) r
i : α
hi : i ∈ ⋃ (n : ι), f n
j : α
hj : j ∈ ⋃ (n : ι), f n
hij : i ≠ j
⊢ r i j
case mpr
α : Type u_1
β : Type ?u.92
γ : Type ?u.95
ι : Type u_2
ι' : Type ?u.101
r p q : α → α → Prop
f✝ g : ι → α
s t u : Set α
a b : α
f : ι → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
⊢ (∀ (n : ι), Set.Pairwise (f n) r) → Set.Pairwise (⋃ (n : ι), f n) r
intro H i hi j hj hij
case mpr.intro
α : Type u_1
β : Type ?u.92
γ : Type ?u.95
ι : Type u_2
ι' : Type ?u.101
r p q : α → α → Prop
f✝ g : ι → α
s t u : Set α
a b : α
f : ι → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
H : ∀ (n : ι), Set.Pairwise (f n) r
i : α
hi : i ∈ ⋃ (n : ι), f n
j : α
hj : j ∈ ⋃ (n : ι), f n
hij : i ≠ j
m : ι
hm : i ∈ f m
⊢ r i j
case mpr
α : Type u_1
β : Type ?u.92
γ : Type ?u.95
ι : Type u_2
ι' : Type ?u.101
r p q : α → α → Prop
f✝ g : ι → α
s t u : Set α
a b : α
f : ι → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
H : ∀ (n : ι), Set.Pairwise (f n) r
i : α
hi : i ∈ ⋃ (n : ι), f n
j : α
hj : j ∈ ⋃ (n : ι), f n
hij : i ≠ j
⊢ r i j
rcases mem_iUnion.1 hi with ⟨m, hm⟩
case mpr.intro.intro
α : Type u_1
β : Type ?u.92
γ : Type ?u.95
ι : Type u_2
ι' : Type ?u.101
r p q : α → α → Prop
f✝ g : ι → α
s t u : Set α
a b : α
f : ι → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
H : ∀ (n : ι), Set.Pairwise (f n) r
i : α
hi : i ∈ ⋃ (n : ι), f n
j : α
hj : j ∈ ⋃ (n : ι), f n
hij : i ≠ j
m : ι
hm : i ∈ f m
n : ι
hn : j ∈ f n
⊢ r i j
case mpr.intro
α : Type u_1
β : Type ?u.92
γ : Type ?u.95
ι : Type u_2
ι' : Type ?u.101
r p q : α → α → Prop
f✝ g : ι → α
s t u : Set α
a b : α
f : ι → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
H : ∀ (n : ι), Set.Pairwise (f n) r
i : α
hi : i ∈ ⋃ (n : ι), f n
j : α
hj : j ∈ ⋃ (n : ι), f n
hij : i ≠ j
m : ι
hm : i ∈ f m
⊢ r i j
rcases mem_iUnion.1 hj with ⟨n, hn⟩
case mpr.intro.intro.intro.intro
α : Type u_1
β : Type ?u.92
γ : Type ?u.95
ι : Type u_2
ι' : Type ?u.101
r p✝ q : α → α → Prop
f✝ g : ι → α
s t u : Set α
a b : α
f : ι → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
H : ∀ (n : ι), Set.Pairwise (f n) r
i : α
hi : i ∈ ⋃ (n : ι), f n
j : α
hj : j ∈ ⋃ (n : ι), f n
hij : i ≠ j
m : ι
hm : i ∈ f m
n : ι
hn : j ∈ f n
p : ι
mp : f m ⊆ f p
np : f n ⊆ f p
⊢ r i j
case mpr.intro.intro
α : Type u_1
β : Type ?u.92
γ : Type ?u.95
ι : Type u_2
ι' : Type ?u.101
r p q : α → α → Prop
f✝ g : ι → α
s t u : Set α
a b : α
f : ι → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
H : ∀ (n : ι), Set.Pairwise (f n) r
i : α
hi : i ∈ ⋃ (n : ι), f n
j : α
hj : j ∈ ⋃ (n : ι), f n
hij : i ≠ j
m : ι
hm : i ∈ f m
n : ι
hn : j ∈ f n
⊢ r i j
rcases h m n with ⟨p, mp, np⟩
no goals
case mpr.intro.intro.intro.intro
α : Type u_1
β : Type ?u.92
γ : Type ?u.95
ι : Type u_2
ι' : Type ?u.101
r p✝ q : α → α → Prop
f✝ g : ι → α
s t u : Set α
a b : α
f : ι → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
H : ∀ (n : ι), Set.Pairwise (f n) r
i : α
hi : i ∈ ⋃ (n : ι), f n
j : α
hj : j ∈ ⋃ (n : ι), f n
hij : i ≠ j
m : ι
hm : i ∈ f m
n : ι
hn : j ∈ f n
p : ι
mp : f m ⊆ f p
np : f n ⊆ f p
⊢ r i j
exact H p (mp hm) (np hn) hij