The values a flat value extends to

Flat.extensions x is the finset of values of a finite type that x extends to: every value for ⊥, and a alone for ↑a. A nonempty finset of values has a most informative flat value extending to all of them, its meet, which is ⊥ once the finset has two values.

Main declarations

• Flat.extensions: the values a flat value extends to.
• Flat.le_inf'_iff_subset_extensions: the meet of a finset of values is the greatest flat value extending to all of them.
• Flat.subset_extensions_iff_eq_bot: only ⊥ extends to two distinct values.
• Flat.finsetInf: the meet of a finset-indexed family of flat values.

theorem Flat.inf'_coe_eq_bot {α : Type u_1} [DecidableEq α] {s : Finset α} (hs : s.Nontrivial) : s.inf' ⋯ some = ⊥

def Flat.finsetInf {α : Type u_1} {ι : Type u_2} [DecidableEq α] (s : Finset ι) (v : ι → Flat α) : Flat α

The meet of the flat values v i over a finset s of indices, ⊥ on the empty finset.

Equations

• Flat.finsetInf s v = if h : s.Nonempty then s.inf' h v else ⊥

@[simp]

theorem Flat.finsetInf_singleton {α : Type u_1} {ι : Type u_2} [DecidableEq α] (i : ι) (v : ι → Flat α) : finsetInf {i} v = v i

def Flat.extensions {α : Type u_1} [DecidableEq α] [Fintype α] (x : Flat α) : Finset α

The values x extends to.

Equations

• x.extensions = {x_1 : α | x ≤ ↑x_1}

@[simp]

theorem Flat.mem_extensions {α : Type u_1} [DecidableEq α] {x : Flat α} {a : α} [Fintype α] : a ∈ x.extensions ↔ x ≤ ↑a

@[simp]

theorem Flat.extensions_bot {α : Type u_1} [DecidableEq α] [Fintype α] : ⊥.extensions = Finset.univ

@[simp]

theorem Flat.extensions_coe {α : Type u_1} [DecidableEq α] [Fintype α] (a : α) : (↑a).extensions = {a}

theorem Flat.le_inf'_iff_subset_extensions {α : Type u_1} [DecidableEq α] {x : Flat α} {s : Finset α} [Fintype α] (hs : s.Nonempty) : x ≤ s.inf' hs some ↔ s ⊆ x.extensions

The meet of a nonempty finset of values is the greatest flat value extending to all of them.

theorem Flat.subset_extensions_iff_eq_bot {α : Type u_1} [DecidableEq α] {x : Flat α} {s : Finset α} [Fintype α] (hs : s.Nontrivial) : s ⊆ x.extensions ↔ x = ⊥