Stream: Is there code for X?

Topic: Get single element from finset

Marcus Rossel (Jan 29 2021 at 14:43):

Is there a way to (a) state that a finset contains exactly one element, and (b) extract that element if (a) is true?

Computably?

Johan Commelin (Jan 29 2021 at 14:43):

Otherwise, s.card = 1

Johan Commelin (Jan 29 2021 at 14:44):

And there must be some lemma that gives s.nonempty from 0 < s.card

Johan Commelin (Jan 29 2021 at 14:45):

If you want to do this computably, you'll have to look at the def'n of finset, and notice that it's basically a list under the hood.

(deleted)

Marcus Rossel (Jan 29 2021 at 14:51):

For the classical path finset.card_eq_one works.

Mario Carneiro (Jan 29 2021 at 14:57):

import data.finset

def multiset.extract_singleton {α} (s : multiset α) : s.card = 1 → α :=
quotient.rec_on s (λ l, match l with [a], _ := a end) $λ a b h, funext$ λ H₂, begin
have H₁ := by rw ← quotient.sound h at H₂; exact H₂,
exact match a, b, H₁, H₂, h :
∀ a b (H₁ : a.length = 1) (H : b.length = 1) (h : list.perm a b), _ with
| [a], [b], _, _, h := begin
rcases h.mem_iff.1 (or.inl rfl) with rfl | ⟨⟨⟩⟩,
refl,
end
end
end

theorem multiset.eq_extract_singleton {α} (s : multiset α) (h) : s = s.extract_singleton h ::ₘ 0 :=
quotient.induction_on s (λ l, match l with [a], _ := rfl end) h

def finset.extract_singleton {α} (s : finset α) (h : s.card = 1) : α :=
s.1.extract_singleton h

theorem finset.eq_extract_singleton {α} (s : finset α) (h) : s = singleton (s.extract_singleton h) :=
finset.eq_of_veq $s.1.eq_extract_singleton h  Eric Wieser (Jan 29 2021 at 15:06): Can docs#finset.choose help here? Eric Wieser (Jan 29 2021 at 15:14): def finset.extract_singleton {α} (s : finset α) (h : s.card = 1) : α := s.choose (set.univ)$ begin
obtain ⟨a, rfl⟩ := finset.card_eq_one.mp h,
refine ⟨a, ⟨finset.mem_singleton_self a, trivial⟩, λ i h, finset.mem_singleton.mp h.1⟩,
end


Last updated: May 17 2021 at 15:13 UTC