Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
/-
Copyright (c) 2020 Adam Topaz. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Adam Topaz

! This file was ported from Lean 3 source module data.set.constructions
! leanprover-community/mathlib commit 9003f28797c0664a49e4179487267c494477d853
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Finset.Basic

/-!
# Constructions involving sets of sets.

## Finite Intersections

We define a structure `FiniteInter` which asserts that a set `S` of subsets of `α` is
closed under finite intersections.

We define `finiteInterClosure` which, given a set `S` of subsets of `α`, is the smallest
set of subsets of `α` which is closed under finite intersections.

`finiteInterClosure S` is endowed with a term of type `FiniteInter` using
`finiteInterClosure_finiteInter`.

-/


variable {
α: Type ?u.169
α
:
Type _: Type (?u.497+1)
Type _
} (
S: Set (Set α)
S
:
Set: Type ?u.500 → Type ?u.500
Set
(
Set: Type ?u.180 → Type ?u.180
Set
α: Type ?u.490
α
)) /-- A structure encapsulating the fact that a set of sets is closed under finite intersection. -/ structure
FiniteInter: {α : Type u_1} → Set (Set α) → Prop
FiniteInter
:
Prop: Type
Prop
where /-- `univ_mem` states that `Set.univ` is in `S`. -/
univ_mem: ∀ {α : Type u_1} {S : Set (Set α)}, FiniteInter S → Set.univ ∈ S
univ_mem
:
Set.univ: {α : Type ?u.34} → Set α
Set.univ
∈
S: Set (Set α)
S
/-- `inter_mem` states that any two intersections of sets in `S` is also in `S`. -/
inter_mem: ∀ {α : Type u_1} {S : Set (Set α)}, FiniteInter S → ∀ ⦃s : Set α⦄, s ∈ S → ∀ ⦃t : Set α⦄, t ∈ S → s ∩ t ∈ S
inter_mem
: ∀ ⦃
s: ?m.54
s
⦄,
s: ?m.54
s
∈
S: Set (Set α)
S
→ ∀ ⦃
t: ?m.86
t
⦄,
t: ?m.86
t
∈
S: Set (Set α)
S
→
s: ?m.54
s
∩
t: ?m.86
t
∈
S: Set (Set α)
S
#align has_finite_inter
FiniteInter: {α : Type u_1} → Set (Set α) → Prop
FiniteInter
namespace FiniteInter /-- The smallest set of sets containing `S` which is closed under finite intersections. -/ inductive
finiteInterClosure: Set (Set α)
finiteInterClosure
:
Set: Type ?u.183 → Type ?u.183
Set
(
Set: Type ?u.184 → Type ?u.184
Set
α: Type ?u.176
α
) |
basic: ∀ {α : Type u_1} {S : Set (Set α)} {s : Set α}, s ∈ S → finiteInterClosure S s
basic
{
s: ?m.189
s
} :
s: ?m.189
s
∈
S: Set (Set α)
S
→
finiteInterClosure: Set (Set α)
finiteInterClosure
s: ?m.189
s
|
univ: ∀ {α : Type u_1} {S : Set (Set α)}, finiteInterClosure S Set.univ
univ
:
finiteInterClosure: Set (Set α)
finiteInterClosure
Set.univ: {α : Type ?u.230} → Set α
Set.univ
|
inter: ∀ {α : Type u_1} {S : Set (Set α)} {s t : Set α}, finiteInterClosure S s → finiteInterClosure S t → finiteInterClosure S (s ∩ t)
inter
{
s: ?m.234
s
t: ?m.237
t
} :
finiteInterClosure: Set (Set α)
finiteInterClosure
s: ?m.234
s
→
finiteInterClosure: Set (Set α)
finiteInterClosure
t: ?m.237
t
→
finiteInterClosure: Set (Set α)
finiteInterClosure
(
s: ?m.234
s
∩
t: ?m.237
t
) #align has_finite_inter.finite_inter_closure
FiniteInter.finiteInterClosure: {α : Type u_1} → Set (Set α) → Set (Set α)
FiniteInter.finiteInterClosure
theorem
finiteInterClosure_finiteInter: ∀ {α : Type u_1} (S : Set (Set α)), FiniteInter (finiteInterClosure S)
finiteInterClosure_finiteInter
:
FiniteInter: {α : Type ?u.504} → Set (Set α) → Prop
FiniteInter
(
finiteInterClosure: {α : Type ?u.506} → Set (Set α) → Set (Set α)
finiteInterClosure
S: Set (Set α)
S
) := { univ_mem :=
finiteInterClosure.univ: ∀ {α : Type ?u.522} {S : Set (Set α)}, finiteInterClosure S Set.univ
finiteInterClosure.univ
inter_mem := fun
_: ?m.532
_
h: ?m.535
h
_: ?m.538
_
=>
finiteInterClosure.inter: ∀ {α : Type ?u.540} {S : Set (Set α)} {s t : Set α}, finiteInterClosure S s → finiteInterClosure S t → finiteInterClosure S (s ∩ t)
finiteInterClosure.inter
h: ?m.535
h
} #align has_finite_inter.finite_inter_closure_has_finite_inter
FiniteInter.finiteInterClosure_finiteInter: ∀ {α : Type u_1} (S : Set (Set α)), FiniteInter (finiteInterClosure S)
FiniteInter.finiteInterClosure_finiteInter
variable {
S: ?m.574
S
} theorem
finiteInter_mem: ∀ {α : Type u_1} {S : Set (Set α)}, FiniteInter S → ∀ (F : Finset (Set α)), ↑F ⊆ S → ⋂₀ ↑F ∈ S
finiteInter_mem
(
cond: FiniteInter S
cond
:
FiniteInter: {α : Type ?u.584} → Set (Set α) → Prop
FiniteInter
S: Set (Set α)
S
) (
F: Finset (Set α)
F
:
Finset: Type ?u.591 → Type ?u.591
Finset
(
Set: Type ?u.592 → Type ?u.592
Set
α: Type ?u.577
α
)) : ↑
F: Finset (Set α)
F
⊆
S: Set (Set α)
S
→ ⋂₀ (↑
F: Finset (Set α)
F
:
Set: Type ?u.636 → Type ?u.636
Set
(
Set: Type ?u.637 → Type ?u.637
Set
α: Type ?u.577
α
)) ∈
S: Set (Set α)
S
:=

Goals accomplished! 🐙
α: Type u_1

S: Set (Set α)

cond: FiniteInter S

F: Finset (Set α)


↑F ⊆ S → ⋂₀ ↑F ∈ S
α: Type u_1

S: Set (Set α)

cond: FiniteInter S

F: Finset (Set α)


↑F ⊆ S → ⋂₀ ↑F ∈ S
α: Type u_1

S: Set (Set α)

cond: FiniteInter S

F: Finset (Set α)

x✝: ↑∅ ⊆ S


refine'_1
α: Type u_1

S: Set (Set α)

cond: FiniteInter S

F: Finset (Set α)


refine'_2
∀ ⦃a : Set α⦄ {s : Finset (Set α)}, ¬a ∈ s → (↑s ⊆ S → ⋂₀ ↑s ∈ S) → ↑(insert a s) ⊆ S → ⋂₀ ↑(insert a s) ∈ S
α: Type u_1

S: Set (Set α)

cond: FiniteInter S

F: Finset (Set α)


↑F ⊆ S → ⋂₀ ↑F ∈ S
α: Type u_1

S: Set (Set α)

cond: FiniteInter S

F: Finset (Set α)

x✝: ↑∅ ⊆ S


refine'_1
α: Type u_1

S: Set (Set α)

cond: FiniteInter S

F: Finset (Set α)

x✝: ↑∅ ⊆ S


refine'_1
α: Type u_1

S: Set (Set α)

cond: FiniteInter S

F: Finset (Set α)


refine'_2
∀ ⦃a : Set α⦄ {s : Finset (Set α)}, ¬a ∈ s → (↑s ⊆ S → ⋂₀ ↑s ∈ S) → ↑(insert a s) ⊆ S → ⋂₀ ↑(insert a s) ∈ S

Goals accomplished! 🐙
α: Type u_1

S: Set (Set α)

cond: FiniteInter S

F: Finset (Set α)


↑F ⊆ S → ⋂₀ ↑F ∈ S
α: Type u_1

S: Set (Set α)

cond: FiniteInter S

F: Finset (Set α)


refine'_2
∀ ⦃a : Set α⦄ {s : Finset (Set α)}, ¬a ∈ s → (↑s ⊆ S → ⋂₀ ↑s ∈ S) → ↑(insert a s) ⊆ S → ⋂₀ ↑(insert a s) ∈ S
α: Type u_1

S: Set (Set α)

cond: FiniteInter S

F: Finset (Set α)


refine'_2
∀ ⦃a : Set α⦄ {s : Finset (Set α)}, ¬a ∈ s → (↑s ⊆ S → ⋂₀ ↑s ∈ S) → ↑(insert a s) ⊆ S → ⋂₀ ↑(insert a s) ∈ S
α: Type u_1

S: Set (Set α)

cond: FiniteInter S

F: Finset (Set α)

a: Set α

s: Finset (Set α)

a✝: ¬a ∈ s

h1: ↑s ⊆ S → ⋂₀ ↑s ∈ S

h2: ↑(insert a s) ⊆ S


refine'_2
⋂₀ ↑(insert a s) ∈ S
α: Type u_1

S: Set (Set α)

cond: FiniteInter S

F: Finset (Set α)


refine'_2
∀ ⦃a : Set α⦄ {s : Finset (Set α)}, ¬a ∈ s → (↑s ⊆ S → ⋂₀ ↑s ∈ S) → ↑(insert a s) ⊆ S → ⋂₀ ↑(insert a s) ∈ S
α: Type u_1

S: Set (Set α)

cond: FiniteInter S

F: Finset (Set α)

a: Set α

s: Finset (Set α)

a✝: ¬a ∈ s

h1: ↑s ⊆ S → ⋂₀ ↑s ∈ S

h2: ↑(insert a s) ⊆ S


refine'_2
⋂₀ ↑(insert a s) ∈ S

Goals accomplished! 🐙
α: Type u_1

S: Set (Set α)

cond: FiniteInter S

F: Finset (Set α)


refine'_2
∀ ⦃a : Set α⦄ {s : Finset (Set α)}, ¬a ∈ s → (↑s ⊆ S → ⋂₀ ↑s ∈ S) → ↑(insert a s) ⊆ S → ⋂₀ ↑(insert a s) ∈ S

Goals accomplished! 🐙
#align has_finite_inter.finite_inter_mem
FiniteInter.finiteInter_mem: ∀ {α : Type u_1} {S : Set (Set α)}, FiniteInter S → ∀ (F : Finset (Set α)), ↑F ⊆ S → ⋂₀ ↑F ∈ S
FiniteInter.finiteInter_mem
theorem
finiteInterClosure_insert: ∀ {A : Set α}, FiniteInter S → ∀ (P : Set α), P ∈ finiteInterClosure (insert A S) → P ∈ S ∨ ∃ Q, Q ∈ S ∧ P = A ∩ Q
finiteInterClosure_insert
{
A: Set α
A
:
Set: Type ?u.1703 → Type ?u.1703
Set
α: Type ?u.1696
α
} (
cond: FiniteInter S
cond
:
FiniteInter: {α : Type ?u.1706} → Set (Set α) → Prop
FiniteInter
S: Set (Set α)
S
) (
P: Set α
P
) (H :
P: ?m.1713
P
∈
finiteInterClosure: {α : Type ?u.1733} → Set (Set α) → Set (Set α)
finiteInterClosure
(
insert: {α : outParam (Type ?u.1737)} → {γ : Type ?u.1736} → [self : Insert α γ] → α → γ → γ
insert
A: Set α
A
S: Set (Set α)
S
)) :
P: ?m.1713
P
∈
S: Set (Set α)
S
∨ ∃
Q: ?m.1793
Q
∈
S: Set (Set α)
S
,
P: ?m.1713
P
=
A: Set α
A
∩
Q: ?m.1793
Q
:=

Goals accomplished! 🐙
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P: Set α

H: P ∈ finiteInterClosure (insert A S)


P ∈ S ∨ ∃ Q, Q ∈ S ∧ P = A ∩ Q
α: Type u_1

S✝: Set (Set α)

A: Set α

cond: FiniteInter S✝

P, S: Set α

h: S ∈ insert A S✝


basic
S ∈ S✝ ∨ ∃ Q, Q ∈ S✝ ∧ S = A ∩ Q
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P: Set α


univ
Set.univ ∈ S ∨ ∃ Q, Q ∈ S ∧ Set.univ = A ∩ Q
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, T1, T2: Set α

a✝¹: finiteInterClosure (insert A S) T1

a✝: finiteInterClosure (insert A S) T2

h1: T1 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 = A ∩ Q

h2: T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T2 = A ∩ Q


inter
T1 ∩ T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ T2 = A ∩ Q
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P: Set α

H: P ∈ finiteInterClosure (insert A S)


P ∈ S ∨ ∃ Q, Q ∈ S ∧ P = A ∩ Q
α: Type u_1

S✝: Set (Set α)

A: Set α

cond: FiniteInter S✝

P, S: Set α

h: S ∈ insert A S✝


basic
S ∈ S✝ ∨ ∃ Q, Q ∈ S✝ ∧ S = A ∩ Q
α: Type u_1

S✝: Set (Set α)

A: Set α

cond: FiniteInter S✝

P, S: Set α

h: S ∈ insert A S✝


basic
S ∈ S✝ ∨ ∃ Q, Q ∈ S✝ ∧ S = A ∩ Q
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P: Set α


univ
Set.univ ∈ S ∨ ∃ Q, Q ∈ S ∧ Set.univ = A ∩ Q
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, T1, T2: Set α

a✝¹: finiteInterClosure (insert A S) T1

a✝: finiteInterClosure (insert A S) T2

h1: T1 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 = A ∩ Q

h2: T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T2 = A ∩ Q


inter
T1 ∩ T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ T2 = A ∩ Q
α: Type u_1

S✝: Set (Set α)

A: Set α

cond: FiniteInter S✝

P, S: Set α

h✝: S = A


basic.inl
S ∈ S✝ ∨ ∃ Q, Q ∈ S✝ ∧ S = A ∩ Q
α: Type u_1

S✝: Set (Set α)

A: Set α

cond: FiniteInter S✝

P, S: Set α

h✝: S ∈ S✝


basic.inr
S ∈ S✝ ∨ ∃ Q, Q ∈ S✝ ∧ S = A ∩ Q
α: Type u_1

S✝: Set (Set α)

A: Set α

cond: FiniteInter S✝

P, S: Set α

h: S ∈ insert A S✝


basic
S ∈ S✝ ∨ ∃ Q, Q ∈ S✝ ∧ S = A ∩ Q
α: Type u_1

S✝: Set (Set α)

A: Set α

cond: FiniteInter S✝

P, S: Set α

h✝: S = A


basic.inl
S ∈ S✝ ∨ ∃ Q, Q ∈ S✝ ∧ S = A ∩ Q
α: Type u_1

S✝: Set (Set α)

A: Set α

cond: FiniteInter S✝

P, S: Set α

h✝: S = A


basic.inl
S ∈ S✝ ∨ ∃ Q, Q ∈ S✝ ∧ S = A ∩ Q
α: Type u_1

S✝: Set (Set α)

A: Set α

cond: FiniteInter S✝

P, S: Set α

h✝: S ∈ S✝


basic.inr
S ∈ S✝ ∨ ∃ Q, Q ∈ S✝ ∧ S = A ∩ Q
α: Type u_1

S✝: Set (Set α)

A: Set α

cond: FiniteInter S✝

P, S: Set α

h✝: S = A


basic.inl
S ∈ S✝ ∨ ∃ Q, Q ∈ S✝ ∧ S = A ∩ Q

Goals accomplished! 🐙
α: Type u_1

S✝: Set (Set α)

A: Set α

cond: FiniteInter S✝

P, S: Set α

h✝: S = A


S = A ∩ Set.univ

Goals accomplished! 🐙

Goals accomplished! 🐙
α: Type u_1

S✝: Set (Set α)

A: Set α

cond: FiniteInter S✝

P, S: Set α

h: S ∈ insert A S✝


basic
S ∈ S✝ ∨ ∃ Q, Q ∈ S✝ ∧ S = A ∩ Q
α: Type u_1

S✝: Set (Set α)

A: Set α

cond: FiniteInter S✝

P, S: Set α

h✝: S ∈ S✝


basic.inr
S ∈ S✝ ∨ ∃ Q, Q ∈ S✝ ∧ S = A ∩ Q
α: Type u_1

S✝: Set (Set α)

A: Set α

cond: FiniteInter S✝

P, S: Set α

h✝: S ∈ S✝


basic.inr
S ∈ S✝ ∨ ∃ Q, Q ∈ S✝ ∧ S = A ∩ Q
α: Type u_1

S✝: Set (Set α)

A: Set α

cond: FiniteInter S✝

P, S: Set α

h✝: S ∈ S✝


basic.inr
S ∈ S✝ ∨ ∃ Q, Q ∈ S✝ ∧ S = A ∩ Q

Goals accomplished! 🐙
α: Type u_1

S✝: Set (Set α)

A: Set α

cond: FiniteInter S✝

P, S: Set α

h✝: S ∈ S✝


S ∈ S✝

Goals accomplished! 🐙

Goals accomplished! 🐙
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P: Set α

H: P ∈ finiteInterClosure (insert A S)


P ∈ S ∨ ∃ Q, Q ∈ S ∧ P = A ∩ Q
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P: Set α


univ
Set.univ ∈ S ∨ ∃ Q, Q ∈ S ∧ Set.univ = A ∩ Q
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P: Set α


univ
Set.univ ∈ S ∨ ∃ Q, Q ∈ S ∧ Set.univ = A ∩ Q
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, T1, T2: Set α

a✝¹: finiteInterClosure (insert A S) T1

a✝: finiteInterClosure (insert A S) T2

h1: T1 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 = A ∩ Q

h2: T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T2 = A ∩ Q


inter
T1 ∩ T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ T2 = A ∩ Q

Goals accomplished! 🐙
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P: Set α

H: P ∈ finiteInterClosure (insert A S)


P ∈ S ∨ ∃ Q, Q ∈ S ∧ P = A ∩ Q
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, T1, T2: Set α

a✝¹: finiteInterClosure (insert A S) T1

a✝: finiteInterClosure (insert A S) T2

h1: T1 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 = A ∩ Q

h2: T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T2 = A ∩ Q


inter
T1 ∩ T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ T2 = A ∩ Q
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, T1, T2: Set α

a✝¹: finiteInterClosure (insert A S) T1

a✝: finiteInterClosure (insert A S) T2

h1: T1 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 = A ∩ Q

h2: T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T2 = A ∩ Q


inter
T1 ∩ T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ T2 = A ∩ Q
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, T1, T2: Set α

a✝¹: finiteInterClosure (insert A S) T1

a✝: finiteInterClosure (insert A S) T2

h2: T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T2 = A ∩ Q

h: T1 ∈ S


inter.inl
T1 ∩ T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ T2 = A ∩ Q
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, T2: Set α

a✝¹: finiteInterClosure (insert A S) T2

h2: T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T2 = A ∩ Q

Q: Set α

hQ: Q ∈ S

a✝: finiteInterClosure (insert A S) (A ∩ Q)


inter.inr.intro.intro
A ∩ Q ∩ T2 ∈ S ∨ ∃ Q_1, Q_1 ∈ S ∧ A ∩ Q ∩ T2 = A ∩ Q_1
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, T1, T2: Set α

a✝¹: finiteInterClosure (insert A S) T1

a✝: finiteInterClosure (insert A S) T2

h1: T1 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 = A ∩ Q

h2: T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T2 = A ∩ Q


inter
T1 ∩ T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ T2 = A ∩ Q
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, T1, T2: Set α

a✝¹: finiteInterClosure (insert A S) T1

a✝: finiteInterClosure (insert A S) T2

h2: T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T2 = A ∩ Q

h: T1 ∈ S


inter.inl
T1 ∩ T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ T2 = A ∩ Q
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, T2: Set α

a✝¹: finiteInterClosure (insert A S) T2

h2: T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T2 = A ∩ Q

Q: Set α

hQ: Q ∈ S

a✝: finiteInterClosure (insert A S) (A ∩ Q)


inter.inr.intro.intro
A ∩ Q ∩ T2 ∈ S ∨ ∃ Q_1, Q_1 ∈ S ∧ A ∩ Q ∩ T2 = A ∩ Q_1
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, T1, T2: Set α

a✝¹: finiteInterClosure (insert A S) T1

a✝: finiteInterClosure (insert A S) T2

h1: T1 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 = A ∩ Q

h2: T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T2 = A ∩ Q


inter
T1 ∩ T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ T2 = A ∩ Q
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, T1, T2: Set α

a✝¹: finiteInterClosure (insert A S) T1

a✝: finiteInterClosure (insert A S) T2

h: T1 ∈ S

i: T2 ∈ S


inter.inl.inl
T1 ∩ T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ T2 = A ∩ Q
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, T1: Set α

a✝¹: finiteInterClosure (insert A S) T1

h: T1 ∈ S

R: Set α

hR: R ∈ S

a✝: finiteInterClosure (insert A S) (A ∩ R)


inter.inl.inr.intro.intro
T1 ∩ (A ∩ R) ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ (A ∩ R) = A ∩ Q
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, T1, T2: Set α

a✝¹: finiteInterClosure (insert A S) T1

a✝: finiteInterClosure (insert A S) T2

h1: T1 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 = A ∩ Q

h2: T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T2 = A ∩ Q


inter
T1 ∩ T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ T2 = A ∩ Q
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, T1, T2: Set α

a✝¹: finiteInterClosure (insert A S) T1

a✝: finiteInterClosure (insert A S) T2

h: T1 ∈ S

i: T2 ∈ S


inter.inl.inl
T1 ∩ T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ T2 = A ∩ Q
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, T1, T2: Set α

a✝¹: finiteInterClosure (insert A S) T1

a✝: finiteInterClosure (insert A S) T2

h: T1 ∈ S

i: T2 ∈ S


inter.inl.inl
T1 ∩ T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ T2 = A ∩ Q
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, T1: Set α

a✝¹: finiteInterClosure (insert A S) T1

h: T1 ∈ S

R: Set α

hR: R ∈ S

a✝: finiteInterClosure (insert A S) (A ∩ R)


inter.inl.inr.intro.intro
T1 ∩ (A ∩ R) ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ (A ∩ R) = A ∩ Q
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, T2: Set α

a✝¹: finiteInterClosure (insert A S) T2

Q: Set α

hQ: Q ∈ S

a✝: finiteInterClosure (insert A S) (A ∩ Q)

i: T2 ∈ S


inter.inr.intro.intro.inl
A ∩ Q ∩ T2 ∈ S ∨ ∃ Q_1, Q_1 ∈ S ∧ A ∩ Q ∩ T2 = A ∩ Q_1
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, Q: Set α

hQ: Q ∈ S

a✝¹: finiteInterClosure (insert A S) (A ∩ Q)

R: Set α

hR: R ∈ S

a✝: finiteInterClosure (insert A S) (A ∩ R)


inter.inr.intro.intro.inr.intro.intro
A ∩ Q ∩ (A ∩ R) ∈ S ∨ ∃ Q_1, Q_1 ∈ S ∧ A ∩ Q ∩ (A ∩ R) = A ∩ Q_1

Goals accomplished! 🐙
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, T1, T2: Set α

a✝¹: finiteInterClosure (insert A S) T1

a✝: finiteInterClosure (insert A S) T2

h1: T1 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 = A ∩ Q

h2: T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T2 = A ∩ Q


inter
T1 ∩ T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ T2 = A ∩ Q
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, T1: Set α

a✝¹: finiteInterClosure (insert A S) T1

h: T1 ∈ S

R: Set α

hR: R ∈ S

a✝: finiteInterClosure (insert A S) (A ∩ R)


inter.inl.inr.intro.intro
T1 ∩ (A ∩ R) ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ (A ∩ R) = A ∩ Q
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, T1: Set α

a✝¹: finiteInterClosure (insert A S) T1

h: T1 ∈ S

R: Set α

hR: R ∈ S

a✝: finiteInterClosure (insert A S) (A ∩ R)


inter.inl.inr.intro.intro
T1 ∩ (A ∩ R) ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ (A ∩ R) = A ∩ Q
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, T2: Set α

a✝¹: finiteInterClosure (insert A S) T2

Q: Set α

hQ: Q ∈ S

a✝: finiteInterClosure (insert A S) (A ∩ Q)

i: T2 ∈ S


inter.inr.intro.intro.inl
A ∩ Q ∩ T2 ∈ S ∨ ∃ Q_1, Q_1 ∈ S ∧ A ∩ Q ∩ T2 = A ∩ Q_1
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, Q: Set α

hQ: Q ∈ S

a✝¹: finiteInterClosure (insert A S) (A ∩ Q)

R: Set α

hR: R ∈ S

a✝: finiteInterClosure (insert A S) (A ∩ R)


inter.inr.intro.intro.inr.intro.intro
A ∩ Q ∩ (A ∩ R) ∈ S ∨ ∃ Q_1, Q_1 ∈ S ∧ A ∩ Q ∩ (A ∩ R) = A ∩ Q_1
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, T1: Set α

a✝¹: finiteInterClosure (insert A S) T1

h: T1 ∈ S

R: Set α

hR: R ∈ S

a✝: finiteInterClosure (insert A S) (A ∩ R)


inter.inl.inr.intro.intro
T1 ∩ (A ∩ R) ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ (A ∩ R) = A ∩ Q

Goals accomplished! 🐙
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, T1: Set α

a✝¹: finiteInterClosure (insert A S) T1

h: T1 ∈ S

R: Set α

hR: R ∈ S

a✝: finiteInterClosure (insert A S) (A ∩ R)


T1 ∩ (A ∩ R) = A ∩ (T1 ∩ R)

Goals accomplished! 🐙

Goals accomplished! 🐙
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, T1, T2: Set α

a✝¹: finiteInterClosure (insert A S) T1

a✝: finiteInterClosure (insert A S) T2

h1: T1 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 = A ∩ Q

h2: T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T2 = A ∩ Q


inter
T1 ∩ T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ T2 = A ∩ Q
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, T2: Set α

a✝¹: finiteInterClosure (insert A S) T2

Q: Set α

hQ: Q ∈ S

a✝: finiteInterClosure (insert A S) (A ∩ Q)

i: T2 ∈ S


inter.inr.intro.intro.inl
A ∩ Q ∩ T2 ∈ S ∨ ∃ Q_1, Q_1 ∈ S ∧ A ∩ Q ∩ T2 = A ∩ Q_1
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, T2: Set α

a✝¹: finiteInterClosure (insert A S) T2

Q: Set α

hQ: Q ∈ S

a✝: finiteInterClosure (insert A S) (A ∩ Q)

i: T2 ∈ S


inter.inr.intro.intro.inl
A ∩ Q ∩ T2 ∈ S ∨ ∃ Q_1, Q_1 ∈ S ∧ A ∩ Q ∩ T2 = A ∩ Q_1
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, Q: Set α

hQ: Q ∈ S

a✝¹: finiteInterClosure (insert A S) (A ∩ Q)

R: Set α

hR: R ∈ S

a✝: finiteInterClosure (insert A S) (A ∩ R)


inter.inr.intro.intro.inr.intro.intro
A ∩ Q ∩ (A ∩ R) ∈ S ∨ ∃ Q_1, Q_1 ∈ S ∧ A ∩ Q ∩ (A ∩ R) = A ∩ Q_1
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, T2: Set α

a✝¹: finiteInterClosure (insert A S) T2

Q: Set α

hQ: Q ∈ S

a✝: finiteInterClosure (insert A S) (A ∩ Q)

i: T2 ∈ S


inter.inr.intro.intro.inl
A ∩ Q ∩ T2 ∈ S ∨ ∃ Q_1, Q_1 ∈ S ∧ A ∩ Q ∩ T2 = A ∩ Q_1

Goals accomplished! 🐙
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, T2: Set α

a✝¹: finiteInterClosure (insert A S) T2

Q: Set α

hQ: Q ∈ S

a✝: finiteInterClosure (insert A S) (A ∩ Q)

i: T2 ∈ S


A ∩ Q ∩ T2 = A ∩ (Q ∩ T2)

Goals accomplished! 🐙

Goals accomplished! 🐙
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, T1, T2: Set α

a✝¹: finiteInterClosure (insert A S) T1

a✝: finiteInterClosure (insert A S) T2

h1: T1 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 = A ∩ Q

h2: T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T2 = A ∩ Q


inter
T1 ∩ T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ T2 = A ∩ Q
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, Q: Set α

hQ: Q ∈ S

a✝¹: finiteInterClosure (insert A S) (A ∩ Q)

R: Set α

hR: R ∈ S

a✝: finiteInterClosure (insert A S) (A ∩ R)


inter.inr.intro.intro.inr.intro.intro
A ∩ Q ∩ (A ∩ R) ∈ S ∨ ∃ Q_1, Q_1 ∈ S ∧ A ∩ Q ∩ (A ∩ R) = A ∩ Q_1
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, Q: Set α

hQ: Q ∈ S

a✝¹: finiteInterClosure (insert A S) (A ∩ Q)

R: Set α

hR: R ∈ S

a✝: finiteInterClosure (insert A S) (A ∩ R)


inter.inr.intro.intro.inr.intro.intro
A ∩ Q ∩ (A ∩ R) ∈ S ∨ ∃ Q_1, Q_1 ∈ S ∧ A ∩ Q ∩ (A ∩ R) = A ∩ Q_1
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, Q: Set α

hQ: Q ∈ S

a✝¹: finiteInterClosure (insert A S) (A ∩ Q)

R: Set α

hR: R ∈ S

a✝: finiteInterClosure (insert A S) (A ∩ R)


inter.inr.intro.intro.inr.intro.intro
A ∩ Q ∩ (A ∩ R) ∈ S ∨ ∃ Q_1, Q_1 ∈ S ∧ A ∩ Q ∩ (A ∩ R) = A ∩ Q_1

Goals accomplished! 🐙
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, Q: Set α

hQ: Q ∈ S

a✝¹: finiteInterClosure (insert A S) (A ∩ Q)

R: Set α

hR: R ∈ S

a✝: finiteInterClosure (insert A S) (A ∩ R)


A ∩ Q ∩ (A ∩ R) = A ∩ (Q ∩ R)
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, Q: Set α

hQ: Q ∈ S

a✝¹: finiteInterClosure (insert A S) (A ∩ Q)

R: Set α

hR: R ∈ S

a✝: finiteInterClosure (insert A S) (A ∩ R)

x: α


h
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, Q: Set α

hQ: Q ∈ S

a✝¹: finiteInterClosure (insert A S) (A ∩ Q)

R: Set α

hR: R ∈ S

a✝: finiteInterClosure (insert A S) (A ∩ R)


A ∩ Q ∩ (A ∩ R) = A ∩ (Q ∩ R)
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, Q: Set α

hQ: Q ∈ S

a✝¹: finiteInterClosure (insert A S) (A ∩ Q)

R: Set α

hR: R ∈ S

a✝: finiteInterClosure (insert A S) (A ∩ R)

x: α


h.mp
x ∈ A ∩ Q ∩ (A ∩ R) → x ∈ A ∩ (Q ∩ R)
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, Q: Set α

hQ: Q ∈ S

a✝¹: finiteInterClosure (insert A S) (A ∩ Q)

R: Set α

hR: R ∈ S

a✝: finiteInterClosure (insert A S) (A ∩ R)

x: α


h.mpr
x ∈ A ∩ (Q ∩ R) → x ∈ A ∩ Q ∩ (A ∩ R)
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, Q: Set α

hQ: Q ∈ S

a✝¹: finiteInterClosure (insert A S) (A ∩ Q)

R: Set α

hR: R ∈ S

a✝: finiteInterClosure (insert A S) (A ∩ R)

x: α


h
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, Q: Set α

hQ: Q ∈ S

a✝¹: finiteInterClosure (insert A S) (A ∩ Q)

R: Set α

hR: R ∈ S

a✝: finiteInterClosure (insert A S) (A ∩ R)

x: α


h.mp
x ∈ A ∩ Q ∩ (A ∩ R) → x ∈ A ∩ (Q ∩ R)
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, Q: Set α

hQ: Q ∈ S

a✝¹: finiteInterClosure (insert A S) (A ∩ Q)

R: Set α

hR: R ∈ S

a✝: finiteInterClosure (insert A S) (A ∩ R)

x: α


h.mpr
x ∈ A ∩ (Q ∩ R) → x ∈ A ∩ Q ∩ (A ∩ R)
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, Q: Set α

hQ: Q ∈ S

a✝¹: finiteInterClosure (insert A S) (A ∩ Q)

R: Set α

hR: R ∈ S

a✝: finiteInterClosure (insert A S) (A ∩ R)

x: α


h

Goals accomplished! 🐙

Goals accomplished! 🐙
#align has_finite_inter.finite_inter_closure_insert
FiniteInter.finiteInterClosure_insert: ∀ {α : Type u_1} {S : Set (Set α)} {A : Set α}, FiniteInter S → ∀ (P : Set α), P ∈ finiteInterClosure (insert A S) → P ∈ S ∨ ∃ Q, Q ∈ S ∧ P = A ∩ Q
FiniteInter.finiteInterClosure_insert
end FiniteInter