Documentation Verification Report

Constructions

📁 Source: Mathlib/Data/Set/Constructions.lean

Statistics

Metric	Count
Definitions `FiniteInter`, `finiteInterClosure`	2
Theorems `finiteInterClosure_finiteInter`, `finiteInterClosure_insert`, `finiteInter_mem`, `inter_mem`, `mk₂`, `univ_mem`, `biUnion_empty_finset`	7
Total	9

FiniteInter

Definitions

Name	Category	Theorems
`finiteInterClosure` 📖	CompData	1 math math: `finiteInterClosure_finiteInter`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finiteInterClosure_finiteInter` 📖	mathematical	—	`FiniteInter` `finiteInterClosure`	—	—
`finiteInterClosure_insert` 📖	mathematical	`FiniteInter` `Set` `Set.instMembership` `finiteInterClosure` `Set.instInsert`	`Set.instInter`	—	`univ_mem` `Set.inter_univ` `inter_mem` `Set.inter_comm` `Set.inter_assoc` `Set.ext`
`finiteInter_mem` 📖	mathematical	`FiniteInter` `Set` `Set.instHasSubset` `SetLike.coe` `Finset` `Finset.instSetLike`	`Set.instMembership` `Set.sInter`	—	`Finset.induction_on` `Finset.coe_empty` `Set.sInter_empty` `univ_mem` `inter_mem` `Finset.mem_insert_self` `Finset.mem_insert_of_mem` `Finset.coe_insert` `Set.sInter_insert`
`inter_mem` 📖	mathematical	`FiniteInter` `Set` `Set.instMembership`	`Set.instInter`	—	—
`mk₂` 📖	mathematical	`Set` `Set.instMembership` `Set.instInter`	`FiniteInter` `Set.instInsert` `Set.univ`	—	`Set.mem_insert` `Set.inter_self` `Set.univ_inter` `Set.inter_univ`
`univ_mem` 📖	mathematical	`FiniteInter`	`Set` `Set.instMembership` `Set.univ`	—	—

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`biUnion_empty_finset` 📖	mathematical	—	`iUnion` `Finset` `Finset.instMembership` `Finset.instEmptyCollection` `Set` `instEmptyCollection`	—	`iUnion_congr_Prop` `iUnion_of_empty` `instIsEmptyFalse` `iUnion_empty`

(root)

Definitions

Name	Category	Theorems
`FiniteInter` 📖	CompData	2 math math: `FiniteInter.finiteInterClosure_finiteInter`, `FiniteInter.mk₂`

---

← Back to Index