Supporting results for pointwise provable equality.

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

The lifted subset relation on optional values.

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

@[instance_reducible]

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

Equations

• PointwiseComposition.Option.instHasSubsetOptionModel = { Subset := PointwiseComposition.Option.IsSubsetOf }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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