Closure properties of team-sets

A team-set T : Set (Finset α) is flat if its membership reduces pointwise: s ∈ T ↔ ∀ w ∈ s, {w} ∈ T. This file states Anttila's Definition 2.2.1 and proves the closure-property characterisation (Anttila Proposition 2.2.2): a flat team-set is downward-closed, sup-closed, and contains ∅.

Over SemilatticeSup-with-OrderBot carriers (which Finset α is) the three closure properties coincide with the data of an Order.IsIdeal: sup-closure ⟺ directedness (via SupClosed.directedOn), and ∅ ∈ T ⟺ T.Nonempty (via IsLowerSet.bot_mem, both in mathlib). This file proves the bridge IsFlat T ↔ Order.IsIdeal T, exposing mathlib's order-ideal infrastructure to consumers of IsFlat.

Main definitions

• Core.Logic.Team.IsFlat T — Anttila's pointwise flatness predicate.

Main results

• Core.Logic.Team.isFlat_iff — Anttila Proposition 2.2.2.
• Core.Logic.Team.isFlat_iff_isIdeal — flat team-sets are precisely the carriers of order-ideals of Finset α.
• Core.Logic.Team.isLowerSet_iff_ordConnected_of_empty — given the empty-team property, downward closure coincides with convexity (Set.OrdConnected). Convexity ([Ant25]) is the closure invariant that survives in the NE-bearing setting where the empty-team property fails. We reuse mathlib's Set.OrdConnected rather than a bespoke predicate, mirroring the IsFlat ↔ Order.IsIdeal bridge.

References

• Anttila, The Logic of Free Choice, MSc thesis 2021, Definition 2.2.1 + Proposition 2.2.2.
• Väänänen, Dependence Logic, Cambridge University Press 2007.

TODO

• Generalise IsFlat to atomistic lattices ([SemilatticeSup L] [OrderBot L] [IsAtomistic L]) once a non-Finset consumer surfaces.

def Core.Logic.Team.IsFlat {α : Type u_1} (T : Set (Finset α)) : Prop

A team-set T : Set (Finset α) is flat iff membership reduces pointwise: s ∈ T ↔ every singleton from s is in T.

Anttila Definition 2.2.1 (the "for all w ∈ s" Yang-Väänänen formulation). Equivalent characterisations: isFlat_iff (via closure properties), isFlat_iff_isIdeal (via Order.IsIdeal).

Equations

• Core.Logic.Team.IsFlat T = ∀ (s : Finset α), s ∈ T ↔ ∀ w ∈ s, {w} ∈ T

theorem Core.Logic.Team.isFlat_iff {α : Type u_1} [DecidableEq α] (T : Set (Finset α)) : IsFlat T ↔ IsLowerSet T ∧ SupClosed T ∧ ∅ ∈ T

Anttila Proposition 2.2.2: a team-set is flat iff it is downward-closed under inclusion, closed under binary union, and contains the empty team.

theorem Core.Logic.Team.isFlat_of_isLowerSet_supClosed_empty {α : Type u_1} [DecidableEq α] {T : Set (Finset α)} (hLower : IsLowerSet T) (hSup : SupClosed T) (hEmpty : ∅ ∈ T) : IsFlat T

theorem Core.Logic.Team.IsFlat.isLowerSet {α : Type u_1} [DecidableEq α] {T : Set (Finset α)} (h : IsFlat T) : IsLowerSet T

theorem Core.Logic.Team.IsFlat.supClosed {α : Type u_1} [DecidableEq α] {T : Set (Finset α)} (h : IsFlat T) : SupClosed T

theorem Core.Logic.Team.IsFlat.empty_mem {α : Type u_1} [DecidableEq α] {T : Set (Finset α)} (h : IsFlat T) : ∅ ∈ T

theorem Core.Logic.Team.isFlat_iff_isIdeal {α : Type u_1} [DecidableEq α] (T : Set (Finset α)) : IsFlat T ↔ Order.IsIdeal T

Anttila Proposition 2.2.2 restated via Order.IsIdeal: flat team-sets are precisely the carriers of order-ideals of Finset α.

Over SemilatticeSup + OrderBot the three closure-property coordinates of IsFlat translate to the three ideal-axiom coordinates: SupClosed ↔ DirectedOn (·≤·) (in SemilatticeSup) and ∅ ∈ T ↔ T.Nonempty (in OrderBot, for lower sets).

Convexity

Convexity — Set.OrdConnected on (Finset α, ⊆), i.e. s ⊆ t ⊆ u with s, u ∈ T forces t ∈ T — is [Ant25]'s generalization of downward closure to the NE-bearing setting where the empty-team property may fail. Mathlib's Set.OrdConnected is exactly this predicate (Set.Icc s u ⊆ T), so we reuse it rather than introduce a bespoke IsConvex, mirroring the IsFlat ↔ Order.IsIdeal reuse above. The forward bridge IsLowerSet.ordConnected is already in mathlib.

theorem Core.Logic.Team.isLowerSet_of_ordConnected_empty {α : Type u_1} {T : Set (Finset α)} (hConv : T.OrdConnected) (hEmpty : ∅ ∈ T) : IsLowerSet T

A convex team-set with the empty-team property is downward-closed — the reverse of mathlib's IsLowerSet.ordConnected. Together they give isLowerSet_iff_ordConnected_of_empty.

theorem Core.Logic.Team.isLowerSet_iff_ordConnected_of_empty {α : Type u_1} {T : Set (Finset α)} (hEmpty : ∅ ∈ T) : IsLowerSet T ↔ T.OrdConnected

Given the empty-team property, downward closure and convexity coincide ([Ant25]). For NE-bearing team-sets — which break the empty-team property — convexity is the invariant that survives where downward closure does not.

theorem Core.Logic.Team.IsFlat.ordConnected {α : Type u_1} [DecidableEq α] {T : Set (Finset α)} (h : IsFlat T) : T.OrdConnected

Flat team-sets are convex (IsFlat → IsLowerSet → OrdConnected).