PreorderRestrict

Statistics

Metric	Count
Definitions	0
Theorems `continuous_frestrictLe`, `continuous_frestrictLe₂`, `continuous_restrictLe`, `continuous_restrictLe₂`	4
Total	4

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_frestrictLe` 📖	mathematical	—	`Continuous` `Pi.topologicalSpace` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Finset.Iic` `frestrictLe`	—	`Finset.continuous_restrict`
`continuous_frestrictLe₂` 📖	mathematical	`toLE`	`Continuous` `Pi.topologicalSpace` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Finset.Iic` `frestrictLe₂`	—	`Finset.continuous_restrict₂`
`continuous_restrictLe` 📖	mathematical	—	`Continuous` `Pi.topologicalSpace` `Set.Elem` `Set.Iic` `Set` `Set.instMembership` `restrictLe`	—	`Pi.continuous_restrict`
`continuous_restrictLe₂` 📖	mathematical	`toLE`	`Continuous` `Pi.topologicalSpace` `Set.Elem` `Set.Iic` `Set` `Set.instMembership` `restrictLe₂`	—	`Pi.continuous_restrict₂`

---