Option lemmas

Lemmas about Option operations such as Option.getD.

Main results

• Option.getD_self_eq_iff: o.getD b = b ↔ ∀ b', o = some b' → b = b'.
• Option.getD_beq_self_eq_true_iff: (o.getD b == b) = true ↔ ∀ b', o = some b' → b = b'.

@[simp]

theorem Option.getD_self_eq_iff {o : Option Bool} {b : Bool} : o.getD b = b ↔ ∀ (b' : Bool), o = some b' → b = b'

An optional Boolean value o agrees with b on the defined part (that is, b = b' whenever o = some b') if and only if o.getD b = b holds.

theorem Option.getD_beq_self_eq_true_iff {o : Option Bool} {b : Bool} : (o.getD b == b) = true ↔ ∀ (b' : Bool), o = some b' → b = b'

An optional Boolean value o agrees with b on the defined part (that is, b = b' whenever o = some b') if and only if o.getD b == b holds.