inductive Option.IsSubsetOf {α : Type u} : Option α → Option α → Prop

• none {α : Type u} {o : Option α} : Option.none.IsSubsetOf o
• some {α : Type u} (a : α) : (Option.some a).IsSubsetOf (Option.some a)

@[instance_reducible]

instance Option.instHasSubset_foundation {α : Type u} : HasSubset (Option α)

Equations

• Option.instHasSubset_foundation = { Subset := Option.IsSubsetOf }

@[simp]

theorem Option.none_subset {α : Type u} (o : Option α) : none ⊆ o

@[simp]

theorem Option.some_subset_some_self {α : Type u} (a : α) : some a ⊆ some a

@[simp]

theorem Option.subset_none_iff {α : Type u} (o : Option α) : o ⊆ none ↔ o = none

@[simp]

theorem Option.some_subset_some {α : Type u} {a b : α} : some a ⊆ some b ↔ a = b

theorem Option.subset_iff {α : Type u} (o₁ o₂ : Option α) : o₁ ⊆ o₂ ↔ ∀ (a : α), a ∈ o₁ → a ∈ o₂