-
Notifications
You must be signed in to change notification settings - Fork 307
/
Finset.lean
114 lines (81 loc) · 4.25 KB
/
Finset.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
/-
Copyright (c) 2018 Sébastien Gouëzel. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Sébastien Gouëzel
-/
import Mathlib.Order.ConditionallyCompleteLattice.Basic
import Mathlib.Data.Set.Finite
#align_import order.conditionally_complete_lattice.finset from "leanprover-community/mathlib"@"2445c98ae4b87eabebdde552593519b9b6dc350c"
/-!
# Conditionally complete lattices and finite sets.
-/
open Set
variable {ι α β γ : Type*}
section ConditionallyCompleteLinearOrder
variable [ConditionallyCompleteLinearOrder α] {s t : Set α} {a b : α}
theorem Finset.Nonempty.csSup_eq_max' {s : Finset α} (h : s.Nonempty) : sSup ↑s = s.max' h :=
eq_of_forall_ge_iff fun _ => (csSup_le_iff s.bddAbove h.to_set).trans (s.max'_le_iff h).symm
#align finset.nonempty.cSup_eq_max' Finset.Nonempty.csSup_eq_max'
theorem Finset.Nonempty.csInf_eq_min' {s : Finset α} (h : s.Nonempty) : sInf ↑s = s.min' h :=
@Finset.Nonempty.csSup_eq_max' αᵒᵈ _ s h
#align finset.nonempty.cInf_eq_min' Finset.Nonempty.csInf_eq_min'
theorem Finset.Nonempty.csSup_mem {s : Finset α} (h : s.Nonempty) : sSup (s : Set α) ∈ s := by
rw [h.csSup_eq_max']
exact s.max'_mem _
#align finset.nonempty.cSup_mem Finset.Nonempty.csSup_mem
theorem Finset.Nonempty.csInf_mem {s : Finset α} (h : s.Nonempty) : sInf (s : Set α) ∈ s :=
@Finset.Nonempty.csSup_mem αᵒᵈ _ _ h
#align finset.nonempty.cInf_mem Finset.Nonempty.csInf_mem
theorem Set.Nonempty.csSup_mem (h : s.Nonempty) (hs : s.Finite) : sSup s ∈ s := by
lift s to Finset α using hs
exact Finset.Nonempty.csSup_mem h
#align set.nonempty.cSup_mem Set.Nonempty.csSup_mem
theorem Set.Nonempty.csInf_mem (h : s.Nonempty) (hs : s.Finite) : sInf s ∈ s :=
@Set.Nonempty.csSup_mem αᵒᵈ _ _ h hs
#align set.nonempty.cInf_mem Set.Nonempty.csInf_mem
theorem Set.Finite.csSup_lt_iff (hs : s.Finite) (h : s.Nonempty) : sSup s < a ↔ ∀ x ∈ s, x < a :=
⟨fun h _ hx => (le_csSup hs.bddAbove hx).trans_lt h, fun H => H _ <| h.csSup_mem hs⟩
#align set.finite.cSup_lt_iff Set.Finite.csSup_lt_iff
theorem Set.Finite.lt_csInf_iff (hs : s.Finite) (h : s.Nonempty) : a < sInf s ↔ ∀ x ∈ s, a < x :=
@Set.Finite.csSup_lt_iff αᵒᵈ _ _ _ hs h
#align set.finite.lt_cInf_iff Set.Finite.lt_csInf_iff
end ConditionallyCompleteLinearOrder
/-!
### Relation between `sSup` / `sInf` and `Finset.sup'` / `Finset.inf'`
Like the `Sup` of a `ConditionallyCompleteLattice`, `Finset.sup'` also requires the set to be
non-empty. As a result, we can translate between the two.
-/
namespace Finset
section ConditionallyCompleteLattice
variable [ConditionallyCompleteLattice α]
theorem sup'_eq_csSup_image (s : Finset ι) (H : s.Nonempty) (f : ι → α) :
s.sup' H f = sSup (f '' s) :=
eq_of_forall_ge_iff fun a => by
simp [csSup_le_iff (s.finite_toSet.image f).bddAbove (H.to_set.image f)]
#align finset.sup'_eq_cSup_image Finset.sup'_eq_csSup_image
#align finset.nonempty.sup'_eq_cSup_image Finset.sup'_eq_csSup_image
theorem inf'_eq_csInf_image (s : Finset ι) (H : s.Nonempty) (f : ι → α) :
s.inf' H f = sInf (f '' s) :=
sup'_eq_csSup_image (α := αᵒᵈ) _ H _
#align finset.inf'_eq_cInf_image Finset.inf'_eq_csInf_image
theorem sup'_id_eq_csSup (s : Finset α) (hs) : s.sup' hs id = sSup s := by
rw [sup'_eq_csSup_image s hs, Set.image_id]
#align finset.sup'_id_eq_cSup Finset.sup'_id_eq_csSup
#align finset.nonempty.sup'_id_eq_cSup Finset.sup'_id_eq_csSup
theorem inf'_id_eq_csInf (s : Finset α) (hs) : s.inf' hs id = sInf s :=
sup'_id_eq_csSup (α := αᵒᵈ) _ hs
#align finset.inf'_id_eq_cInf Finset.inf'_id_eq_csInf
variable [Fintype ι] [Nonempty ι]
lemma sup'_univ_eq_ciSup (f : ι → α) : univ.sup' univ_nonempty f = ⨆ i, f i := by
simp [sup'_eq_csSup_image, iSup]
lemma inf'_univ_eq_ciInf (f : ι → α) : univ.inf' univ_nonempty f = ⨅ i, f i := by
simp [inf'_eq_csInf_image, iInf]
end ConditionallyCompleteLattice
section ConditionallyCompleteLinearOrderBot
variable [ConditionallyCompleteLinearOrderBot α]
lemma sup_univ_eq_ciSup [Fintype ι] (f : ι → α) : univ.sup f = ⨆ i, f i :=
le_antisymm
(Finset.sup_le fun _ _ => le_ciSup (finite_range _).bddAbove _)
(ciSup_le' fun _ => Finset.le_sup (mem_univ _))
end ConditionallyCompleteLinearOrderBot
end Finset