ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → DecidableEq (β i)<VAR>x y : (i : ι) → β i<GOAL>0 < hammingDist x y ↔ x ≠ y
<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → DecidableEq (β i)<VAR>x y : (i : ι) → β i<GOAL>hammingDist x y < 1 ↔ x = y
<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → DecidableEq (β i)<VAR>x y : (i : ι) → β i<GOAL>hammingDist x y ≤ Fintype.card ι
<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → DecidableEq (β i)<VAR>γ : ι → Type u_4<VAR>(i : ι) → DecidableEq (γ i)<VAR>f : (i : ι) → γ i → β i<VAR>x y : (i : ι) → γ i<GOAL>(hammingDist (fun i => f i (x i)) fun i => f i (y i)) ≤ hammingDist x y
<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → DecidableEq (β i)<VAR>γ : ι → Type u_4<VAR>(i : ι) → DecidableEq (γ i)<VAR>f : (i : ι) → γ i → β i<VAR>x y : (i : ι) → γ i<VAR>hf : ∀ (i : ι), Function.Injective (f i)<GOAL>(hammingDist (fun i => f i (x i)) fun i => f i (y i)) = hammingDist x y
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → DecidableEq (β i)<VAR>(i : ι) → SMul α (β i)<VAR>k : α<VAR>x y : (i : ι) → β i<GOAL>hammingDist (k • x) (k • y) ≤ hammingDist x y
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → DecidableEq (β i)<VAR>(i : ι) → SMul α (β i)<VAR>k : α<VAR>x y : (i : ι) → β i<VAR>hk : ∀ (i : ι), IsSMulRegular (β i) k<GOAL>hammingDist (k • x) (k • y) = hammingDist x y
<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → DecidableEq (β i)<VAR>(i : ι) → Zero (β i)<VAR>x : (i : ι) → β i<GOAL>hammingDist x 0 = hammingNorm x
<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → DecidableEq (β i)<VAR>(i : ι) → Zero (β i)<GOAL>hammingDist 0 = hammingNorm
<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → DecidableEq (β i)<VAR>(i : ι) → Zero (β i)<VAR>x : (i : ι) → β i<GOAL>0 ≤ hammingNorm x
<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → DecidableEq (β i)<VAR>(i : ι) → Zero (β i)<GOAL>hammingNorm 0 = 0
<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → DecidableEq (β i)<VAR>(i : ι) → Zero (β i)<VAR>x : (i : ι) → β i<GOAL>hammingNorm x = 0 ↔ x = 0
<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → DecidableEq (β i)<VAR>(i : ι) → Zero (β i)<VAR>x : (i : ι) → β i<GOAL>hammingNorm x ≠ 0 ↔ x ≠ 0
<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → DecidableEq (β i)<VAR>(i : ι) → Zero (β i)<VAR>x : (i : ι) → β i<GOAL>0 < hammingNorm x ↔ x ≠ 0
<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → DecidableEq (β i)<VAR>(i : ι) → Zero (β i)<VAR>x : (i : ι) → β i<GOAL>hammingNorm x < 1 ↔ x = 0
<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → DecidableEq (β i)<VAR>(i : ι) → Zero (β i)<VAR>x : (i : ι) → β i<GOAL>hammingNorm x ≤ Fintype.card ι
<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → DecidableEq (β i)<VAR>γ : ι → Type u_4<VAR>(i : ι) → DecidableEq (γ i)<VAR>(i : ι) → Zero (β i)<VAR>(i : ι) → Zero (γ i)<VAR>f : (i : ι) → γ i → β i<VAR>x : (i : ι) → γ i<VAR>hf : ∀ (i : ι), f i 0 = 0<GOAL>(hammingNorm fun i => f i (x i)) ≤ hammingNorm x
<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → DecidableEq (β i)<VAR>γ : ι → Type u_4<VAR>(i : ι) → DecidableEq (γ i)<VAR>(i : ι) → Zero (β i)<VAR>(i : ι) → Zero (γ i)<VAR>f : (i : ι) → γ i → β i<VAR>x : (i : ι) → γ i<VAR>hf₁ : ∀ (i : ι), Function.Injective (f i)<VAR>hf₂ : ∀ (i : ι), f i 0 = 0<GOAL>(hammingNorm fun i => f i (x i)) = hammingNorm x
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → DecidableEq (β i)<VAR>(i : ι) → Zero (β i)<VAR>Zero α<VAR>(i : ι) → SMulWithZero α (β i)<VAR>k : α<VAR>x : (i : ι) → β i<GOAL>hammingNorm (k • x) ≤ hammingNorm x
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → DecidableEq (β i)<VAR>(i : ι) → Zero (β i)<VAR>Zero α<VAR>(i : ι) → SMulWithZero α (β i)<VAR>k : α<VAR>hk : ∀ (i : ι), IsSMulRegular (β i) k<VAR>x : (i : ι) → β i<GOAL>hammingNorm (k • x) = hammingNorm x
<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → DecidableEq (β i)<VAR>(i : ι) → AddGroup (β i)<VAR>x y : (i : ι) → β i<GOAL>hammingDist x y = hammingNorm (x - y)
<VAR>ι : Type u_2<VAR>β : ι → Type u_3<GOAL>Hamming.toHamming.symm = Hamming.ofHamming
<VAR>ι : Type u_2<VAR>β : ι → Type u_3<GOAL>Hamming.ofHamming.symm = Hamming.toHamming
<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>x : Hamming β<GOAL>Hamming.toHamming (Hamming.ofHamming x) = x
<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>x : (i : ι) → β i<GOAL>Hamming.ofHamming (Hamming.toHamming x) = x
<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>x y : (i : ι) → β i<GOAL>Hamming.toHamming x = Hamming.toHamming y ↔ x = y
<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>x y : Hamming β<GOAL>Hamming.ofHamming x = Hamming.ofHamming y ↔ x = y
<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>(i : ι) → Zero (β i)<GOAL>Hamming.toHamming 0 = 0
<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>(i : ι) → Zero (β i)<GOAL>Hamming.ofHamming 0 = 0
<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>(i : ι) → Neg (β i)<VAR>x : (i : ι) → β i<GOAL>Hamming.toHamming (-x) = -Hamming.toHamming x
<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>(i : ι) → Neg (β i)<VAR>x : Hamming β<GOAL>Hamming.ofHamming (-x) = -Hamming.ofHamming x
<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>(i : ι) → Add (β i)<VAR>x y : (i : ι) → β i<GOAL>Hamming.toHamming (x + y) = Hamming.toHamming x + Hamming.toHamming y
<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>(i : ι) → Add (β i)<VAR>x y : Hamming β<GOAL>Hamming.ofHamming (x + y) = Hamming.ofHamming x + Hamming.ofHamming y
<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>(i : ι) → Sub (β i)<VAR>x y : (i : ι) → β i<GOAL>Hamming.toHamming (x - y) = Hamming.toHamming x - Hamming.toHamming y
<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>(i : ι) → Sub (β i)<VAR>x y : Hamming β<GOAL>Hamming.ofHamming (x - y) = Hamming.ofHamming x - Hamming.ofHamming y
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>(i : ι) → SMul α (β i)<VAR>r : α<VAR>x : (i : ι) → β i<GOAL>Hamming.toHamming (r • x) = r • Hamming.toHamming x
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>(i : ι) → SMul α (β i)<VAR>r : α<VAR>x : Hamming β<GOAL>Hamming.ofHamming (r • x) = r • Hamming.ofHamming x
<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → DecidableEq (β i)<VAR>x y : Hamming β<GOAL>dist x y = ↑(hammingDist (Hamming.ofHamming x) (Hamming.ofHamming y))
<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → DecidableEq (β i)<VAR>x y : Hamming β<GOAL>nndist x y = ↑(hammingDist (Hamming.ofHamming x) (Hamming.ofHamming y))
<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → DecidableEq (β i)<VAR>(i : ι) → Zero (β i)<VAR>x : Hamming β<GOAL>‖x‖ = ↑(hammingNorm (Hamming.ofHamming x))
<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → DecidableEq (β i)<VAR>(i : ι) → AddCommGroup (β i)<VAR>x : Hamming β<GOAL>‖x‖₊ = ↑(hammingNorm (Hamming.ofHamming x))
<VAR>α : Sort u<VAR>β : α → Sort v<VAR>r : α → α → Prop<VAR>s : (a : α) → β a → β a → Prop<VAR>ha : WellFounded r<VAR>hb : ∀ (x : α), WellFounded (s x)<GOAL>WellFounded (PSigma.Lex r s)
<VAR>α : Type u<VAR>β : Type v<VAR>s : β → β → Prop<VAR>hb : WellFounded s<GOAL>WellFounded (PSigma.SkipLeft α s)
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>{x | a < x ∧ x < b} = Set.Ioo a b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>{x | a ≤ x ∧ x < b} = Set.Ico a b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>{x | x < a} = Set.Iio a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>{x | a ≤ x ∧ x ≤ b} = Set.Icc a b
<VAR>α : Type u_1<VAR>Preorder α<VAR>b : α<GOAL>{x | x ≤ b} = Set.Iic b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>{x | a < x ∧ x ≤ b} = Set.Ioc a b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>{x | a ≤ x} = Set.Ici a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>{x | a < x} = Set.Ioi a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b x : α<GOAL>x ∈ Set.Ioo a b ↔ a < x ∧ x < b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b x : α<GOAL>x ∈ Set.Ico a b ↔ a ≤ x ∧ x < b
<VAR>α : Type u_1<VAR>Preorder α<VAR>b x : α<GOAL>x ∈ Set.Iio b ↔ x < b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b x : α<GOAL>x ∈ Set.Icc a b ↔ a ≤ x ∧ x ≤ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>b x : α<GOAL>x ∈ Set.Iic b ↔ x ≤ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b x : α<GOAL>x ∈ Set.Ioc a b ↔ a < x ∧ x ≤ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a x : α<GOAL>x ∈ Set.Ici a ↔ a ≤ x
<VAR>α : Type u_1<VAR>Preorder α<VAR>a x : α<GOAL>x ∈ Set.Ioi a ↔ a < x
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>a ∈ Set.Ioo a b ↔ False
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>a ∈ Set.Ico a b ↔ a < b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>a ∈ Set.Icc a b ↔ a ≤ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>a ∈ Set.Ioc a b ↔ False
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>a ∈ Set.Ici a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>b ∈ Set.Ioo a b ↔ False
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>b ∈ Set.Ico a b ↔ False
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>b ∈ Set.Icc a b ↔ a ≤ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>b ∈ Set.Ioc a b ↔ a < b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>a ∈ Set.Iic a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>Set.Ici (OrderDual.toDual a) = ⇑OrderDual.ofDual ⁻¹' Set.Iic a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>Set.Iic (OrderDual.toDual a) = ⇑OrderDual.ofDual ⁻¹' Set.Ici a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>Set.Ioi (OrderDual.toDual a) = ⇑OrderDual.ofDual ⁻¹' Set.Iio a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>Set.Iio (OrderDual.toDual a) = ⇑OrderDual.ofDual ⁻¹' Set.Ioi a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>Set.Icc (OrderDual.toDual a) (OrderDual.toDual b) = ⇑OrderDual.ofDual ⁻¹' Set.Icc b a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>Set.Ioc (OrderDual.toDual a) (OrderDual.toDual b) = ⇑OrderDual.ofDual ⁻¹' Set.Ico b a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>Set.Ico (OrderDual.toDual a) (OrderDual.toDual b) = ⇑OrderDual.ofDual ⁻¹' Set.Ioc b a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>Set.Ioo (OrderDual.toDual a) (OrderDual.toDual b) = ⇑OrderDual.ofDual ⁻¹' Set.Ioo b a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>(Set.Icc a b).Nonempty ↔ a ≤ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>(Set.Ico a b).Nonempty ↔ a < b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>(Set.Ioc a b).Nonempty ↔ a < b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>(Set.Ici a).Nonempty
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>(Set.Iic a).Nonempty
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<VAR>DenselyOrdered α<GOAL>(Set.Ioo a b).Nonempty ↔ a < b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<VAR>NoMaxOrder α<GOAL>(Set.Ioi a).Nonempty
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<VAR>NoMinOrder α<GOAL>(Set.Iio a).Nonempty
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>Nonempty ↑(Set.Icc a b)
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<VAR>h : a < b<GOAL>Nonempty ↑(Set.Ico a b)
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<VAR>h : a < b<GOAL>Nonempty ↑(Set.Ioc a b)
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<VAR>DenselyOrdered α<VAR>h : a < b<GOAL>Nonempty ↑(Set.Ioo a b)
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<VAR>h : ¬a ≤ b<GOAL>Set.Icc a b = ∅
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<VAR>h : ¬a < b<GOAL>Set.Ico a b = ∅
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<VAR>h : ¬a < b<GOAL>Set.Ioc a b = ∅
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<VAR>h : ¬a < b<GOAL>Set.Ioo a b = ∅
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<VAR>h : b < a<GOAL>Set.Icc a b = ∅
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<VAR>h : b ≤ a<GOAL>Set.Ico a b = ∅
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<VAR>h : b ≤ a<GOAL>Set.Ioc a b = ∅
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<VAR>h : b ≤ a<GOAL>Set.Ioo a b = ∅
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>Set.Ico a a = ∅
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>Set.Ioc a a = ∅
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>Set.Ioo a a = ∅
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>Set.Ici a ⊆ Set.Ici b ↔ b ≤ a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>Set.Iic a ⊆ Set.Iic b ↔ a ≤ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>Set.Ici a ⊆ Set.Ioi b ↔ b < a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>Set.Iic a ⊆ Set.Iio b ↔ a < b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a₁ a₂ b₁ b₂ : α<VAR>h₁ : a₂ ≤ a₁<VAR>h₂ : b₁ ≤ b₂<GOAL>Set.Ioo a₁ b₁ ⊆ Set.Ioo a₂ b₂
<VAR>α : Type u_1<VAR>Preorder α<VAR>a₁ a₂ b : α<VAR>h : a₁ ≤ a₂<GOAL>Set.Ioo a₂ b ⊆ Set.Ioo a₁ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b₁ b₂ : α<VAR>h : b₁ ≤ b₂<GOAL>Set.Ioo a b₁ ⊆ Set.Ioo a b₂
<VAR>α : Type u_1<VAR>Preorder α<VAR>a₁ a₂ b₁ b₂ : α<VAR>h₁ : a₂ ≤ a₁<VAR>h₂ : b₁ ≤ b₂<GOAL>Set.Ico a₁ b₁ ⊆ Set.Ico a₂ b₂
<VAR>α : Type u_1<VAR>Preorder α<VAR>a₁ a₂ b : α<VAR>h : a₁ ≤ a₂<GOAL>Set.Ico a₂ b ⊆ Set.Ico a₁ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b₁ b₂ : α<VAR>h : b₁ ≤ b₂<GOAL>Set.Ico a b₁ ⊆ Set.Ico a b₂
<VAR>α : Type u_1<VAR>Preorder α<VAR>a₁ a₂ b₁ b₂ : α<VAR>h₁ : a₂ ≤ a₁<VAR>h₂ : b₁ ≤ b₂<GOAL>Set.Icc a₁ b₁ ⊆ Set.Icc a₂ b₂
<VAR>α : Type u_1<VAR>Preorder α<VAR>a₁ a₂ b : α<VAR>h : a₁ ≤ a₂<GOAL>Set.Icc a₂ b ⊆ Set.Icc a₁ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b₁ b₂ : α<VAR>h : b₁ ≤ b₂<GOAL>Set.Icc a b₁ ⊆ Set.Icc a b₂
<VAR>α : Type u_1<VAR>Preorder α<VAR>a₁ a₂ b₁ b₂ : α<VAR>ha : a₂ < a₁<VAR>hb : b₁ < b₂<GOAL>Set.Icc a₁ b₁ ⊆ Set.Ioo a₂ b₂
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>Set.Icc a b ⊆ Set.Ici a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>Set.Icc a b ⊆ Set.Iic b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>Set.Ioc a b ⊆ Set.Iic b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a₁ a₂ b₁ b₂ : α<VAR>h₁ : a₂ ≤ a₁<VAR>h₂ : b₁ ≤ b₂<GOAL>Set.Ioc a₁ b₁ ⊆ Set.Ioc a₂ b₂
<VAR>α : Type u_1<VAR>Preorder α<VAR>a₁ a₂ b : α<VAR>h : a₁ ≤ a₂<GOAL>Set.Ioc a₂ b ⊆ Set.Ioc a₁ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b₁ b₂ : α<VAR>h : b₁ ≤ b₂<GOAL>Set.Ioc a b₁ ⊆ Set.Ioc a b₂
<VAR>α : Type u_1<VAR>Preorder α<VAR>a₁ a₂ b : α<VAR>h₁ : a₁ < a₂<GOAL>Set.Ico a₂ b ⊆ Set.Ioo a₁ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b₁ b₂ : α<VAR>h : b₁ < b₂<GOAL>Set.Ioc a b₁ ⊆ Set.Ioo a b₂
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b₁ b₂ : α<VAR>h₁ : b₁ < b₂<GOAL>Set.Icc a b₁ ⊆ Set.Ico a b₂
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>Set.Ioo a b ⊆ Set.Ico a b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>Set.Ioo a b ⊆ Set.Ioc a b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>Set.Ico a b ⊆ Set.Icc a b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>Set.Ioc a b ⊆ Set.Icc a b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>Set.Ioo a b ⊆ Set.Icc a b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>Set.Ico a b ⊆ Set.Iio b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>Set.Ioo a b ⊆ Set.Iio b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>Set.Ioc a b ⊆ Set.Ioi a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>Set.Ioo a b ⊆ Set.Ioi a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>Set.Ioi a ⊆ Set.Ici a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>Set.Iio a ⊆ Set.Iic a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>Set.Ico a b ⊆ Set.Ici a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>Set.Ioi a ⊂ Set.Ici a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>Set.Iio a ⊂ Set.Iic a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a₁ a₂ b₁ b₂ : α<VAR>h₁ : a₁ ≤ b₁<GOAL>Set.Icc a₁ b₁ ⊆ Set.Icc a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂
<VAR>α : Type u_1<VAR>Preorder α<VAR>a₁ a₂ b₁ b₂ : α<VAR>h₁ : a₁ ≤ b₁<GOAL>Set.Icc a₁ b₁ ⊆ Set.Ioo a₂ b₂ ↔ a₂ < a₁ ∧ b₁ < b₂
<VAR>α : Type u_1<VAR>Preorder α<VAR>a₁ a₂ b₁ b₂ : α<VAR>h₁ : a₁ ≤ b₁<GOAL>Set.Icc a₁ b₁ ⊆ Set.Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ < b₂
<VAR>α : Type u_1<VAR>Preorder α<VAR>a₁ a₂ b₁ b₂ : α<VAR>h₁ : a₁ ≤ b₁<GOAL>Set.Icc a₁ b₁ ⊆ Set.Ioc a₂ b₂ ↔ a₂ < a₁ ∧ b₁ ≤ b₂
<VAR>α : Type u_1<VAR>Preorder α<VAR>a₁ b₁ b₂ : α<VAR>h₁ : a₁ ≤ b₁<GOAL>Set.Icc a₁ b₁ ⊆ Set.Iio b₂ ↔ b₁ < b₂
<VAR>α : Type u_1<VAR>Preorder α<VAR>a₁ a₂ b₁ : α<VAR>h₁ : a₁ ≤ b₁<GOAL>Set.Icc a₁ b₁ ⊆ Set.Ioi a₂ ↔ a₂ < a₁
<VAR>α : Type u_1<VAR>Preorder α<VAR>a₁ b₁ b₂ : α<VAR>h₁ : a₁ ≤ b₁<GOAL>Set.Icc a₁ b₁ ⊆ Set.Iic b₂ ↔ b₁ ≤ b₂
<VAR>α : Type u_1<VAR>Preorder α<VAR>a₁ a₂ b₁ : α<VAR>h₁ : a₁ ≤ b₁<GOAL>Set.Icc a₁ b₁ ⊆ Set.Ici a₂ ↔ a₂ ≤ a₁
<VAR>α : Type u_1<VAR>Preorder α<VAR>a₁ a₂ b₁ b₂ : α<VAR>hI : a₂ ≤ b₂<VAR>ha : a₂ < a₁<VAR>hb : b₁ ≤ b₂<GOAL>Set.Icc a₁ b₁ ⊂ Set.Icc a₂ b₂
<VAR>α : Type u_1<VAR>Preorder α<VAR>a₁ a₂ b₁ b₂ : α<VAR>hI : a₂ ≤ b₂<VAR>ha : a₂ ≤ a₁<VAR>hb : b₁ < b₂<GOAL>Set.Icc a₁ b₁ ⊂ Set.Icc a₂ b₂
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>Set.Ioi b ⊆ Set.Ioi a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>Set.Ioi b ⊆ Set.Ici a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>Set.Iio a ⊆ Set.Iio b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>Set.Iio a ⊆ Set.Iic b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>Set.Ici a ∩ Set.Iic b = Set.Icc a b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>Set.Ici a ∩ Set.Iio b = Set.Ico a b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>Set.Ioi a ∩ Set.Iic b = Set.Ioc a b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>Set.Ioi a ∩ Set.Iio b = Set.Ioo a b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>Set.Iic a ∩ Set.Ici b = Set.Icc b a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>Set.Iio a ∩ Set.Ici b = Set.Ico b a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>Set.Iic a ∩ Set.Ioi b = Set.Ioc b a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>Set.Iio a ∩ Set.Ioi b = Set.Ioo b a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b x : α<VAR>h : x ∈ Set.Ioo a b<GOAL>x ∈ Set.Icc a b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b x : α<VAR>h : x ∈ Set.Ioo a b<GOAL>x ∈ Set.Ico a b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b x : α<VAR>h : x ∈ Set.Ioo a b<GOAL>x ∈ Set.Ioc a b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b x : α<VAR>h : x ∈ Set.Ico a b<GOAL>x ∈ Set.Icc a b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b x : α<VAR>h : x ∈ Set.Ioc a b<GOAL>x ∈ Set.Icc a b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a x : α<VAR>h : x ∈ Set.Ioi a<GOAL>x ∈ Set.Ici a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a x : α<VAR>h : x ∈ Set.Iio a<GOAL>x ∈ Set.Iic a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>Set.Icc a b = ∅ ↔ ¬a ≤ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>Set.Ico a b = ∅ ↔ ¬a < b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>Set.Ioc a b = ∅ ↔ ¬a < b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<VAR>DenselyOrdered α<GOAL>Set.Ioo a b = ∅ ↔ ¬a < b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<VAR>h : IsTop a<GOAL>Set.Iic a = Set.univ
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<VAR>h : IsBot a<GOAL>Set.Ici a = Set.univ
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<VAR>h : IsMax a<GOAL>Set.Ioi a = ∅
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<VAR>h : IsMin a<GOAL>Set.Iio a = ∅
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b c : α<VAR>h : a ≤ c<GOAL>Set.Iic a ∩ Set.Ioc b c = Set.Ioc b a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b c : α<VAR>ha : c < a<GOAL>c ∉ Set.Icc a b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b c : α<VAR>hb : b < c<GOAL>c ∉ Set.Icc a b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b c : α<VAR>ha : c < a<GOAL>c ∉ Set.Ico a b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b c : α<VAR>hb : b < c<GOAL>c ∉ Set.Ioc a b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>a ∉ Set.Ioi a
<VAR>α : Type u_1<VAR>Preorder α<VAR>b : α<GOAL>b ∉ Set.Iio b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b c : α<VAR>ha : c ≤ a<GOAL>c ∉ Set.Ioc a b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b c : α<VAR>hb : b ≤ c<GOAL>c ∉ Set.Ico a b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b c : α<VAR>ha : c ≤ a<GOAL>c ∉ Set.Ioo a b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b c : α<VAR>hb : b ≤ c<GOAL>c ∉ Set.Ioo a b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a : α<GOAL>Set.Icc a a = {a}
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a b c : α<GOAL>Set.Icc a b = {c} ↔ a = c ∧ b = c
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a b : α<VAR>hba : b ≤ a<GOAL>(Set.Icc a b).Subsingleton
<VAR>α : Type u_3<VAR>LinearOrder α<VAR>a b : α<GOAL>(Set.Icc a b).Subsingleton ↔ b ≤ a
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a b : α<GOAL>Set.Icc a b \ {a} = Set.Ioc a b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a b : α<GOAL>Set.Icc a b \ {b} = Set.Ico a b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a b : α<GOAL>Set.Ico a b \ {a} = Set.Ioo a b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a b : α<GOAL>Set.Ioc a b \ {b} = Set.Ioo a b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a b : α<GOAL>Set.Icc a b \ {a, b} = Set.Ioo a b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a : α<GOAL>Set.Ici a \ {a} = Set.Ioi a
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a : α<GOAL>Set.Iic a \ {a} = Set.Iio a
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a b : α<VAR>h : a < b<GOAL>Set.Ico a b \ Set.Ioo a b = {a}
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a b : α<VAR>h : a < b<GOAL>Set.Ioc a b \ Set.Ioo a b = {b}
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>Set.Icc a b \ Set.Ico a b = {b}
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>Set.Icc a b \ Set.Ioc a b = {a}
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>Set.Icc a b \ Set.Ioo a b = {a, b}
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a : α<GOAL>Set.Ici a \ Set.Ioi a = {a}
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a : α<GOAL>Set.Iic a \ Set.Iio a = {a}
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a : α<GOAL>Set.Ioi a ∪ {a} = Set.Ici a
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a : α<GOAL>Set.Iio a ∪ {a} = Set.Iic a
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a b : α<VAR>hab : a < b<GOAL>Set.Ioo a b ∪ {a} = Set.Ico a b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a b : α<VAR>hab : a < b<GOAL>Set.Ioo a b ∪ {b} = Set.Ioc a b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>Set.Ioo a b ∪ {a, b} = Set.Icc a b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a b : α<VAR>hab : a ≤ b<GOAL>Set.Ioc a b ∪ {a} = Set.Icc a b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a b : α<VAR>hab : a ≤ b<GOAL>Set.Ico a b ∪ {b} = Set.Icc a b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>insert b (Set.Ico a b) = Set.Icc a b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>insert a (Set.Ioc a b) = Set.Icc a b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a b : α<VAR>h : a < b<GOAL>insert a (Set.Ioo a b) = Set.Ico a b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a b : α<VAR>h : a < b<GOAL>insert b (Set.Ioo a b) = Set.Ioc a b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a : α<GOAL>insert a (Set.Iio a) = Set.Iic a
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a : α<GOAL>insert a (Set.Ioi a) = Set.Ici a
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a : α<VAR>s : Set α<VAR>ho : Set.Ioi a ⊆ s<VAR>hc : s ⊆ Set.Ici a<GOAL>s ∈ {Set.Ici a, Set.Ioi a}
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a : α<VAR>s : Set α<VAR>ho : Set.Iio a ⊆ s<VAR>hc : s ⊆ Set.Iic a<GOAL>s ∈ {Set.Iic a, Set.Iio a}
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a b : α<VAR>s : Set α<VAR>ho : Set.Ioo a b ⊆ s<VAR>hc : s ⊆ Set.Icc a b<GOAL>s ∈ {Set.Icc a b, Set.Ico a b, Set.Ioc a b, Set.Ioo a b}
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a b x : α<VAR>hmem : x ∈ Set.Ico a b<GOAL>x = a ∨ x ∈ Set.Ioo a b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a b x : α<VAR>hmem : x ∈ Set.Ioc a b<GOAL>x = b ∨ x ∈ Set.Ioo a b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a b x : α<VAR>hmem : x ∈ Set.Icc a b<GOAL>x = a ∨ x = b ∨ x ∈ Set.Ioo a b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a : α<VAR>h : IsMax a<GOAL>Set.Ici a = {a}
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a : α<VAR>h : IsMin a<GOAL>Set.Iic a = {a}
<VAR>α : Type u_1<VAR>PartialOrder α<GOAL>Function.Injective Set.Ici
<VAR>α : Type u_1<VAR>PartialOrder α<GOAL>Function.Injective Set.Iic
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a b : α<GOAL>Set.Ici a = Set.Ici b ↔ a = b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a b : α<GOAL>Set.Iic a = Set.Iic b ↔ a = b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>OrderTop α<GOAL>Set.Ici ⊤ = {⊤}
<VAR>α : Type u_1<VAR>Preorder α<VAR>OrderTop α<GOAL>Set.Ioi ⊤ = ∅
<VAR>α : Type u_1<VAR>Preorder α<VAR>OrderTop α<GOAL>Set.Iic ⊤ = Set.univ
<VAR>α : Type u_1<VAR>Preorder α<VAR>OrderTop α<VAR>a : α<GOAL>Set.Icc a ⊤ = Set.Ici a
<VAR>α : Type u_1<VAR>Preorder α<VAR>OrderTop α<VAR>a : α<GOAL>Set.Ioc a ⊤ = Set.Ioi a
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>OrderBot α<GOAL>Set.Iic ⊥ = {⊥}