Zulip Chat Archive

Stream: new members

Topic: What does two dots mean in front of an identifier


view this post on Zulip Lars Ericson (Dec 09 2020 at 18:07):

What does the last line of this mean, in particular the .. in ..induced_outer_measure :

def of_measurable {α} [measurable_space α]
  (m : Π (s : set α), is_measurable s  ennreal)
  (m0 : m  is_measurable.empty = 0)
  (mU :  {{f :   set α}} (h : i, is_measurable (f i)),
    pairwise (disjoint on f) 
    m (i, f i) (is_measurable.Union h) = (∑'i, m (f i) (h i))) :
  measure α :=
{ m_Union := λ f hf hd,
  show induced_outer_measure m _ m0 (Union f) =
      ∑' i, induced_outer_measure m _ m0 (f i), begin
    rw [induced_outer_measure_eq m0 mU, mU hf hd],
    congr, funext n, rw induced_outer_measure_eq m0 mU
  end,
  trimmed :=
  show (induced_outer_measure m _ m0).trim = induced_outer_measure m _ m0, begin
    unfold outer_measure.trim,
    congr, funext s hs,
    exact induced_outer_measure_eq m0 mU hs
  end,
  ..induced_outer_measure m _ m0 }

view this post on Zulip Eric Wieser (Dec 09 2020 at 18:15):

Unpack the fields of the structure to the right of the dots into the containing structure

view this post on Zulip Bryan Gin-ge Chen (Dec 09 2020 at 18:18):

This is called the "record update syntax" in 9.2 of TPiL.


Last updated: May 12 2021 at 23:13 UTC