Commit 2023-01-17 17:59 5d7cd872

View on Github →

feat: port Order.SupIndep (#1627)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/SupIndep.lean

added theorem CompleteLattice.Independent.comp'

added theorem CompleteLattice.Independent.comp

added theorem CompleteLattice.Independent.disjoint_bsupᵢ

added theorem CompleteLattice.Independent.injective

added theorem CompleteLattice.Independent.map_orderIso

added theorem CompleteLattice.Independent.mono

added theorem CompleteLattice.Independent.pairwiseDisjoint

added theorem CompleteLattice.Independent.setIndependent_range

added def CompleteLattice.Independent

added theorem CompleteLattice.SetIndependent.disjoint_supₛ

added theorem CompleteLattice.SetIndependent.mono

added theorem CompleteLattice.SetIndependent.pairwiseDisjoint

added def CompleteLattice.SetIndependent

added theorem CompleteLattice.independent_def''

added theorem CompleteLattice.independent_def'

added theorem CompleteLattice.independent_def

added theorem CompleteLattice.independent_empty

added theorem CompleteLattice.independent_iff_pairwiseDisjoint

added theorem CompleteLattice.independent_iff_supIndep

added theorem CompleteLattice.independent_iff_supIndep_univ

added theorem CompleteLattice.independent_map_orderIso_iff

added theorem CompleteLattice.independent_pair

added theorem CompleteLattice.independent_pempty

added theorem CompleteLattice.setIndependent_empty

added theorem CompleteLattice.setIndependent_iff

added theorem CompleteLattice.setIndependent_iff_pairwiseDisjoint

added theorem CompleteLattice.setIndependent_pair

added theorem Finset.SupIndep.attach

added theorem Finset.SupIndep.bunionᵢ

added theorem Finset.SupIndep.pairwiseDisjoint

added theorem Finset.SupIndep.subset

added theorem Finset.SupIndep.sup

added def Finset.SupIndep

added theorem Finset.supIndep_empty

added theorem Finset.supIndep_iff_disjoint_erase

added theorem Finset.supIndep_iff_pairwiseDisjoint

added theorem Finset.supIndep_pair

added theorem Finset.supIndep_singleton

added theorem Finset.supIndep_univ_bool

added theorem Finset.supIndep_univ_fin_two