class FiniteCharacter {α : Type u_1} (s : Set (Set α)) : Prop

• mem_iff_finite_subset_mem : ∀ {x : Set α}, x ∈ s ↔ ∀ (y : Set α), y ⊆ x → Finite ↥y → y ∈ s

theorem mem_iff_finite_subset_mem {α : Type u_1} {s : Set (Set α)} [FiniteCharacter s] {x : Set α} : x ∈ s ↔ ∀ (y : Set α), y ⊆ x → Finite ↥y → y ∈ s

instance instFiniteCharacterEmptyCollectionSet {α : Type u_1} : FiniteCharacter ∅

Equations

• ⋯ = ⋯

instance instFiniteCharacterUnivSet {α : Type u_1} : FiniteCharacter Set.univ

Equations

• ⋯ = ⋯

instance instFiniteCharacterInterSet {α : Type u_1} {s t : Set (Set α)} [FiniteCharacter s] [FiniteCharacter t] : FiniteCharacter (s ∩ t)

Equations

• ⋯ = ⋯

instance instFiniteCharacterIInterSet {α : Type u_1} {ι : Type u_2} {s : ι → Set (Set α)} [∀ (i : ι), FiniteCharacter (s i)] : FiniteCharacter (⋂ i : ι, s i)

Equations

• ⋯ = ⋯

instance totally_ordered_finiteCharacter {α : Type u_1} [PartialOrder α] : FiniteCharacter {s : Set α | ∀ (x y : ↥s), Comparable x y}

Equations

• ⋯ = ⋯

instance FiniteCharacter.inductiveOrder {α : Type u_1} {s : Set (Set α)} [FiniteCharacter s] (ne : s.Nonempty) : InductiveOrder ↥s

Equations

• ⋯ = ⋯

theorem FiniteCharacter.has_maximal {α : Type u_1} {s : Set (Set α)} (h : FiniteCharacter s) (ne : s.Nonempty) : ∃ (x : ↥s), Maximal x